Theorem isofrlem 2939

Description: Lemma for isofr 2940.

Assertion

Ref	Expression
isofrlem	⊢ (H Isom R, S (A, B) → (S Fr B → R Fr A))

Proof of Theorem isofrlem

Step	Hyp	Ref	Expression
1		isof1o 2931	. . . . . . 7 ⊢ (H Isom R, S (A, B) → H:A–1-1-onto→B)
2		f1ofun 2802	. . . . . . 7 ⊢ (H:A–1-1-onto→B → Fun H)
3		visset 1350	. . . . . . . . 9 ⊢ x ∈ V
4	3	funimaex 2716	. . . . . . . 8 ⊢ (Fun H → (H “ x) ∈ V)
5		sseq1 1521	. . . . . . . . . . 11 ⊢ (z = (H “ x) → (z ⊆ B ↔ (H “ x) ⊆ B))
6		cleq1 1107	. . . . . . . . . . . 12 ⊢ (z = (H “ x) → (z = ∅ ↔ (H “ x) = ∅))
7	6	negbid 463	. . . . . . . . . . 11 ⊢ (z = (H “ x) → (¬ z = ∅ ↔ ¬ (H “ x) = ∅))
8	5, 7	anbi12d 476	. . . . . . . . . 10 ⊢ (z = (H “ x) → ((z ⊆ B ∧ ¬ z = ∅) ↔ ((H “ x) ⊆ B ∧ ¬ (H “ x) = ∅)))
9		ineq1 1638	. . . . . . . . . . . 12 ⊢ (z = (H “ x) → (z ∩ (◡S “ {w})) = ((H “ x) ∩ (◡S “ {w})))
10	9	cleq1d 1109	. . . . . . . . . . 11 ⊢ (z = (H “ x) → ((z ∩ (◡S “ {w})) = ∅ ↔ ((H “ x) ∩ (◡S “ {w})) = ∅))
11	10	rexeqd 1328	. . . . . . . . . 10 ⊢ (z = (H “ x) → (∃w ∈ z (z ∩ (◡S “ {w})) = ∅ ↔ ∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅))
12	8, 11	imbi12d 474	. . . . . . . . 9 ⊢ (z = (H “ x) → (((z ⊆ B ∧ ¬ z = ∅) → ∃w ∈ z (z ∩ (◡S “ {w})) = ∅) ↔ (((H “ x) ⊆ B ∧ ¬ (H “ x) = ∅) → ∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅)))
13	12	cla4gv 1396	. . . . . . . 8 ⊢ ((H “ x) ∈ V → (∀z((z ⊆ B ∧ ¬ z = ∅) → ∃w ∈ z (z ∩ (◡S “ {w})) = ∅) → (((H “ x) ⊆ B ∧ ¬ (H “ x) = ∅) → ∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅)))
14	4, 13	syl 12	. . . . . . 7 ⊢ (Fun H → (∀z((z ⊆ B ∧ ¬ z = ∅) → ∃w ∈ z (z ∩ (◡S “ {w})) = ∅) → (((H “ x) ⊆ B ∧ ¬ (H “ x) = ∅) → ∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅)))
15	1, 2, 14	3syl 21	. . . . . 6 ⊢ (H Isom R, S (A, B) → (∀z((z ⊆ B ∧ ¬ z = ∅) → ∃w ∈ z (z ∩ (◡S “ {w})) = ∅) → (((H “ x) ⊆ B ∧ ¬ (H “ x) = ∅) → ∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅)))
16		dffr3 2620	. . . . . 6 ⊢ (S Fr B ↔ ∀z((z ⊆ B ∧ ¬ z = ∅) → ∃w ∈ z (z ∩ (◡S “ {w})) = ∅))
17	15, 16	syl5ib 181	. . . . 5 ⊢ (H Isom R, S (A, B) → (S Fr B → (((H “ x) ⊆ B ∧ ¬ (H “ x) = ∅) → ∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅)))
18		f1ofo 2806	. . . . . . . . 9 ⊢ (H:A–1-1-onto→B → H:A–onto→B)
19		imassrn 2611	. . . . . . . . . 10 ⊢ (H “ x) ⊆ ran H
20		forn 2789	. . . . . . . . . . 11 ⊢ (H:A–onto→B → ran H = B)
21	20	sseq2d 1528	. . . . . . . . . 10 ⊢ (H:A–onto→B → ((H “ x) ⊆ ran H ↔ (H “ x) ⊆ B))
22	19, 21	mpbii 168	. . . . . . . . 9 ⊢ (H:A–onto→B → (H “ x) ⊆ B)
23	18, 22	syl 12	. . . . . . . 8 ⊢ (H:A–1-1-onto→B → (H “ x) ⊆ B)
24	23	a1d 14	. . . . . . 7 ⊢ (H:A–1-1-onto→B → ((x ⊆ A ∧ ¬ x = ∅) → (H “ x) ⊆ B))
25		f1ofn 2801	. . . . . . . 8 ⊢ (H:A–1-1-onto→B → H Fn A)
26		ssel 1502	. . . . . . . . . . . . . 14 ⊢ (x ⊆ A → (y ∈ x → y ∈ A))
27		funfvima 2904	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun H ∧ y ∈ dom H) → (y ∈ x → (H ‘y) ∈ (H “ x)))
28	27	funfni 2724	. . . . . . . . . . . . . . . 16 ⊢ ((H Fn A ∧ y ∈ A) → (y ∈ x → (H ‘y) ∈ (H “ x)))
29		n0i 1712	. . . . . . . . . . . . . . . 16 ⊢ ((H ‘y) ∈ (H “ x) → ¬ (H “ x) = ∅)
30	28, 29	syl6 23	. . . . . . . . . . . . . . 15 ⊢ ((H Fn A ∧ y ∈ A) → (y ∈ x → ¬ (H “ x) = ∅))
31	30	exp 291	. . . . . . . . . . . . . 14 ⊢ (H Fn A → (y ∈ A → (y ∈ x → ¬ (H “ x) = ∅)))
32	26, 31	sylan9r 360	. . . . . . . . . . . . 13 ⊢ ((H Fn A ∧ x ⊆ A) → (y ∈ x → (y ∈ x → ¬ (H “ x) = ∅)))
33	32	pm2.43d 59	. . . . . . . . . . . 12 ⊢ ((H Fn A ∧ x ⊆ A) → (y ∈ x → ¬ (H “ x) = ∅))
34	33	19.23adv 954	. . . . . . . . . . 11 ⊢ ((H Fn A ∧ x ⊆ A) → (∃y y ∈ x → ¬ (H “ x) = ∅))
35		n0 1714	. . . . . . . . . . 11 ⊢ (¬ x = ∅ ↔ ∃y y ∈ x)
36	34, 35	syl5ib 181	. . . . . . . . . 10 ⊢ ((H Fn A ∧ x ⊆ A) → (¬ x = ∅ → ¬ (H “ x) = ∅))
37	36	exp 291	. . . . . . . . 9 ⊢ (H Fn A → (x ⊆ A → (¬ x = ∅ → ¬ (H “ x) = ∅)))
38	37	imp3a 279	. . . . . . . 8 ⊢ (H Fn A → ((x ⊆ A ∧ ¬ x = ∅) → ¬ (H “ x) = ∅))
39	25, 38	syl 12	. . . . . . 7 ⊢ (H:A–1-1-onto→B → ((x ⊆ A ∧ ¬ x = ∅) → ¬ (H “ x) = ∅))
40	24, 39	jcad 455	. . . . . 6 ⊢ (H:A–1-1-onto→B → ((x ⊆ A ∧ ¬ x = ∅) → ((H “ x) ⊆ B ∧ ¬ (H “ x) = ∅)))
41	1, 40	syl 12	. . . . 5 ⊢ (H Isom R, S (A, B) → ((x ⊆ A ∧ ¬ x = ∅) → ((H “ x) ⊆ B ∧ ¬ (H “ x) = ∅)))
42	17, 41	syl5d 53	. . . 4 ⊢ (H Isom R, S (A, B) → (S Fr B → ((x ⊆ A ∧ ¬ x = ∅) → ∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅)))
43		fvelima 2859	. . . . . . . . . . 11 ⊢ ((Fun H ∧ w ∈ (H “ x)) → ∃y ∈ x (H ‘y) = w)
44	1	adantr 306	. . . . . . . . . . . 12 ⊢ ((H Isom R, S (A, B) ∧ x ⊆ A) → H:A–1-1-onto→B)
45	44, 2	syl 12	. . . . . . . . . . 11 ⊢ ((H Isom R, S (A, B) ∧ x ⊆ A) → Fun H)
46		pm3.26 256	. . . . . . . . . . 11 ⊢ ((w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅) → w ∈ (H “ x))
47	43, 45, 46	syl2an 349	. . . . . . . . . 10 ⊢ (((H Isom R, S (A, B) ∧ x ⊆ A) ∧ (w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅)) → ∃y ∈ x (H ‘y) = w)
48		isomin 2937	. . . . . . . . . . . . . . . . . . 19 ⊢ ((H Isom R, S (A, B) ∧ (x ⊆ A ∧ y ∈ A)) → ((x ∩ (◡R “ {y})) = ∅ ↔ ((H “ x) ∩ (◡S “ {(H ‘y)})) = ∅))
49	26	imdistani 340	. . . . . . . . . . . . . . . . . . 19 ⊢ ((x ⊆ A ∧ y ∈ x) → (x ⊆ A ∧ y ∈ A))
50	48, 49	sylan2 346	. . . . . . . . . . . . . . . . . 18 ⊢ ((H Isom R, S (A, B) ∧ (x ⊆ A ∧ y ∈ x)) → ((x ∩ (◡R “ {y})) = ∅ ↔ ((H “ x) ∩ (◡S “ {(H ‘y)})) = ∅))
51		sneq 1816	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((H ‘y) = w → {(H ‘y)} = {w})
52		imaeq2 2603	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({(H ‘y)} = {w} → (◡S “ {(H ‘y)}) = (◡S “ {w}))
53	51, 52	syl 12	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((H ‘y) = w → (◡S “ {(H ‘y)}) = (◡S “ {w}))
54	53	ineq2d 1645	. . . . . . . . . . . . . . . . . . 19 ⊢ ((H ‘y) = w → ((H “ x) ∩ (◡S “ {(H ‘y)})) = ((H “ x) ∩ (◡S “ {w})))
55	54	cleq1d 1109	. . . . . . . . . . . . . . . . . 18 ⊢ ((H ‘y) = w → (((H “ x) ∩ (◡S “ {(H ‘y)})) = ∅ ↔ ((H “ x) ∩ (◡S “ {w})) = ∅))
56	50, 55	sylan9bb 418	. . . . . . . . . . . . . . . . 17 ⊢ (((H Isom R, S (A, B) ∧ (x ⊆ A ∧ y ∈ x)) ∧ (H ‘y) = w) → ((x ∩ (◡R “ {y})) = ∅ ↔ ((H “ x) ∩ (◡S “ {w})) = ∅))
57		pm3.27 260	. . . . . . . . . . . . . . . . 17 ⊢ ((w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅) → ((H “ x) ∩ (◡S “ {w})) = ∅)
58	56, 57	syl5bir 184	. . . . . . . . . . . . . . . 16 ⊢ (((H Isom R, S (A, B) ∧ (x ⊆ A ∧ y ∈ x)) ∧ (H ‘y) = w) → ((w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅) → (x ∩ (◡R “ {y})) = ∅))
59	58	exp42 300	. . . . . . . . . . . . . . 15 ⊢ (H Isom R, S (A, B) → (x ⊆ A → (y ∈ x → ((H ‘y) = w → ((w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅) → (x ∩ (◡R “ {y})) = ∅)))))
60	59	imp 277	. . . . . . . . . . . . . 14 ⊢ ((H Isom R, S (A, B) ∧ x ⊆ A) → (y ∈ x → ((H ‘y) = w → ((w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅) → (x ∩ (◡R “ {y})) = ∅))))
61	60	com3l 34	. . . . . . . . . . . . 13 ⊢ (y ∈ x → ((H ‘y) = w → ((H Isom R, S (A, B) ∧ x ⊆ A) → ((w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅) → (x ∩ (◡R “ {y})) = ∅))))
62	61	com4t 40	. . . . . . . . . . . 12 ⊢ ((H Isom R, S (A, B) ∧ x ⊆ A) → ((w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅) → (y ∈ x → ((H ‘y) = w → (x ∩ (◡R “ {y})) = ∅))))
63	62	imp 277	. . . . . . . . . . 11 ⊢ (((H Isom R, S (A, B) ∧ x ⊆ A) ∧ (w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅)) → (y ∈ x → ((H ‘y) = w → (x ∩ (◡R “ {y})) = ∅)))
64	63	r19.22dv 1278	. . . . . . . . . 10 ⊢ (((H Isom R, S (A, B) ∧ x ⊆ A) ∧ (w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅)) → (∃y ∈ x (H ‘y) = w → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅))
65	47, 64	mpd 46	. . . . . . . . 9 ⊢ (((H Isom R, S (A, B) ∧ x ⊆ A) ∧ (w ∈ (H “ x) ∧ ((H “ x) ∩ (◡S “ {w})) = ∅)) → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅)
66	65	exp32 294	. . . . . . . 8 ⊢ ((H Isom R, S (A, B) ∧ x ⊆ A) → (w ∈ (H “ x) → (((H “ x) ∩ (◡S “ {w})) = ∅ → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅)))
67	66	r19.23adv 1286	. . . . . . 7 ⊢ ((H Isom R, S (A, B) ∧ x ⊆ A) → (∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅ → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅))
68	67	exp 291	. . . . . 6 ⊢ (H Isom R, S (A, B) → (x ⊆ A → (∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅ → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅)))
69	68	adantrd 308	. . . . 5 ⊢ (H Isom R, S (A, B) → ((x ⊆ A ∧ ¬ x = ∅) → (∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅ → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅)))
70	69	a2d 15	. . . 4 ⊢ (H Isom R, S (A, B) → (((x ⊆ A ∧ ¬ x = ∅) → ∃w ∈ (H “ x)((H “ x) ∩ (◡S “ {w})) = ∅) → ((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅)))
71	42, 70	syld 27	. . 3 ⊢ (H Isom R, S (A, B) → (S Fr B → ((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅)))
72	71	19.21adv 945	. 2 ⊢ (H Isom R, S (A, B) → (S Fr B → ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅)))
73		dffr3 2620	. 2 ⊢ (R Fr A ↔ ∀x((x ⊆ A ∧ ¬ x = ∅) → ∃y ∈ x (x ∩ (◡R “ {y})) = ∅))
74	72, 73	syl6ibr 186	1 ⊢ (H Isom R, S (A, B) → (S Fr B → R Fr A))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348   ∩ cin 1486   ⊆ wss 1487  ∅c0 1707  {csn 1808   Fr wfr 2061  ^◡ccnv 2409  ran crn 2411   “ cima 2413  Fun wfun 2416   Fn wfn 2417  –onto→wfo 2420  –1-1-onto→wf1o 2421   ‘cfv 2422   Isom wiso 2423

This theorem is referenced by:  isofr 2940

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-fr 2169  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fo 2436  df-f1o 2437  df-fv 2438  df-iso 2439

metamath.org