Theorem isomin 2937

Description: Isomorphisms preserve minimal elements. Note that (^◡R “ {D}) is Takeuti and Zaring's idiom for the initial segment {x∣xRD}. Proposition 6.31(1) of [TakeutiZaring] p. 33.

Assertion

Ref	Expression
isomin	⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → ((C ∩ (◡R “ {D})) = ∅ ↔ ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅))

Proof of Theorem isomin

Step	Hyp	Ref	Expression
1		ssel 1502	. . . . . . . . . . . . . 14 ⊢ (C ⊆ A → (x ∈ C → x ∈ A))
2		isof1o 2931	. . . . . . . . . . . . . . 15 ⊢ (H Isom R, S (A, B) → H:A–1-1-onto→B)
3		f1ofn 2801	. . . . . . . . . . . . . . 15 ⊢ (H:A–1-1-onto→B → H Fn A)
4		visset 1350	. . . . . . . . . . . . . . . . 17 ⊢ y ∈ V
5	4	fnfvbr 2855	. . . . . . . . . . . . . . . 16 ⊢ ((H Fn A ∧ x ∈ A) → ((H ‘x) = y ↔ xHy))
6	5	exp 291	. . . . . . . . . . . . . . 15 ⊢ (H Fn A → (x ∈ A → ((H ‘x) = y ↔ xHy)))
7	2, 3, 6	3syl 21	. . . . . . . . . . . . . 14 ⊢ (H Isom R, S (A, B) → (x ∈ A → ((H ‘x) = y ↔ xHy)))
8	1, 7	syl9r 56	. . . . . . . . . . . . 13 ⊢ (H Isom R, S (A, B) → (C ⊆ A → (x ∈ C → ((H ‘x) = y ↔ xHy))))
9	8	imp31 280	. . . . . . . . . . . 12 ⊢ (((H Isom R, S (A, B) ∧ C ⊆ A) ∧ x ∈ C) → ((H ‘x) = y ↔ xHy))
10	9	birexdva 1216	. . . . . . . . . . 11 ⊢ ((H Isom R, S (A, B) ∧ C ⊆ A) → (∃x ∈ C (H ‘x) = y ↔ ∃x ∈ C xHy))
11	4	elima 2606	. . . . . . . . . . 11 ⊢ (y ∈ (H “ C) ↔ ∃x ∈ C xHy)
12	10, 11	syl6rbbr 417	. . . . . . . . . 10 ⊢ ((H Isom R, S (A, B) ∧ C ⊆ A) → (y ∈ (H “ C) ↔ ∃x ∈ C (H ‘x) = y))
13		fvex 2838	. . . . . . . . . . . 12 ⊢ (H ‘D) ∈ V
14	4	eliniseg 2618	. . . . . . . . . . . 12 ⊢ ((H ‘D) ∈ V → (y ∈ (◡S “ {(H ‘D)}) ↔ yS(H ‘D)))
15	13, 14	ax-mp 6	. . . . . . . . . . 11 ⊢ (y ∈ (◡S “ {(H ‘D)}) ↔ yS(H ‘D))
16	15	a1i 7	. . . . . . . . . 10 ⊢ ((H Isom R, S (A, B) ∧ C ⊆ A) → (y ∈ (◡S “ {(H ‘D)}) ↔ yS(H ‘D)))
17	12, 16	anbi12d 476	. . . . . . . . 9 ⊢ ((H Isom R, S (A, B) ∧ C ⊆ A) → ((y ∈ (H “ C) ∧ y ∈ (◡S “ {(H ‘D)})) ↔ (∃x ∈ C (H ‘x) = y ∧ yS(H ‘D))))
18		elin 1635	. . . . . . . . 9 ⊢ (y ∈ ((H “ C) ∩ (◡S “ {(H ‘D)})) ↔ (y ∈ (H “ C) ∧ y ∈ (◡S “ {(H ‘D)})))
19		r19.41v 1302	. . . . . . . . 9 ⊢ (∃x ∈ C ((H ‘x) = y ∧ yS(H ‘D)) ↔ (∃x ∈ C (H ‘x) = y ∧ yS(H ‘D)))
20	17, 18, 19	3bitr4g 428	. . . . . . . 8 ⊢ ((H Isom R, S (A, B) ∧ C ⊆ A) → (y ∈ ((H “ C) ∩ (◡S “ {(H ‘D)})) ↔ ∃x ∈ C ((H ‘x) = y ∧ yS(H ‘D))))
21	20	adantrr 312	. . . . . . 7 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (y ∈ ((H “ C) ∩ (◡S “ {(H ‘D)})) ↔ ∃x ∈ C ((H ‘x) = y ∧ yS(H ‘D))))
22		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ x ∈ V
23	22	eliniseg 2618	. . . . . . . . . . . . . . 15 ⊢ (D ∈ A → (x ∈ (◡R “ {D}) ↔ xRD))
24	23	ad2antrr 323	. . . . . . . . . . . . . 14 ⊢ ((H Isom R, S (A, B) ∧ (x ∈ A ∧ D ∈ A)) → (x ∈ (◡R “ {D}) ↔ xRD))
25		isorel 2932	. . . . . . . . . . . . . 14 ⊢ ((H Isom R, S (A, B) ∧ (x ∈ A ∧ D ∈ A)) → (xRD ↔ (H ‘x)S(H ‘D)))
26	24, 25	bitrd 406	. . . . . . . . . . . . 13 ⊢ ((H Isom R, S (A, B) ∧ (x ∈ A ∧ D ∈ A)) → (x ∈ (◡R “ {D}) ↔ (H ‘x)S(H ‘D)))
27		breq1 2065	. . . . . . . . . . . . . 14 ⊢ ((H ‘x) = y → ((H ‘x)S(H ‘D) ↔ yS(H ‘D)))
28	27	biimpar 325	. . . . . . . . . . . . 13 ⊢ (((H ‘x) = y ∧ yS(H ‘D)) → (H ‘x)S(H ‘D))
29	26, 28	syl5bir 184	. . . . . . . . . . . 12 ⊢ ((H Isom R, S (A, B) ∧ (x ∈ A ∧ D ∈ A)) → (((H ‘x) = y ∧ yS(H ‘D)) → x ∈ (◡R “ {D})))
30	29	exp32 294	. . . . . . . . . . 11 ⊢ (H Isom R, S (A, B) → (x ∈ A → (D ∈ A → (((H ‘x) = y ∧ yS(H ‘D)) → x ∈ (◡R “ {D})))))
31	1, 30	syl9r 56	. . . . . . . . . 10 ⊢ (H Isom R, S (A, B) → (C ⊆ A → (x ∈ C → (D ∈ A → (((H ‘x) = y ∧ yS(H ‘D)) → x ∈ (◡R “ {D}))))))
32	31	com34 36	. . . . . . . . 9 ⊢ (H Isom R, S (A, B) → (C ⊆ A → (D ∈ A → (x ∈ C → (((H ‘x) = y ∧ yS(H ‘D)) → x ∈ (◡R “ {D}))))))
33	32	imp32 281	. . . . . . . 8 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (x ∈ C → (((H ‘x) = y ∧ yS(H ‘D)) → x ∈ (◡R “ {D}))))
34	33	r19.22dv 1278	. . . . . . 7 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (∃x ∈ C ((H ‘x) = y ∧ yS(H ‘D)) → ∃x ∈ C x ∈ (◡R “ {D})))
35	21, 34	sylbid 178	. . . . . 6 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (y ∈ ((H “ C) ∩ (◡S “ {(H ‘D)})) → ∃x ∈ C x ∈ (◡R “ {D})))
36		elin 1635	. . . . . . . 8 ⊢ (x ∈ (C ∩ (◡R “ {D})) ↔ (x ∈ C ∧ x ∈ (◡R “ {D})))
37	36	biex 733	. . . . . . 7 ⊢ (∃x x ∈ (C ∩ (◡R “ {D})) ↔ ∃x(x ∈ C ∧ x ∈ (◡R “ {D})))
38		n0 1714	. . . . . . 7 ⊢ (¬ (C ∩ (◡R “ {D})) = ∅ ↔ ∃x x ∈ (C ∩ (◡R “ {D})))
39		df-rex 1206	. . . . . . 7 ⊢ (∃x ∈ C x ∈ (◡R “ {D}) ↔ ∃x(x ∈ C ∧ x ∈ (◡R “ {D})))
40	37, 38, 39	3bitr4 158	. . . . . 6 ⊢ (¬ (C ∩ (◡R “ {D})) = ∅ ↔ ∃x ∈ C x ∈ (◡R “ {D}))
41	35, 40	syl6ibr 186	. . . . 5 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (y ∈ ((H “ C) ∩ (◡S “ {(H ‘D)})) → ¬ (C ∩ (◡R “ {D})) = ∅))
42	41	19.23adv 954	. . . 4 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (∃y y ∈ ((H “ C) ∩ (◡S “ {(H ‘D)})) → ¬ (C ∩ (◡R “ {D})) = ∅))
43		n0 1714	. . . 4 ⊢ (¬ ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅ ↔ ∃y y ∈ ((H “ C) ∩ (◡S “ {(H ‘D)})))
44	42, 43	syl5ib 181	. . 3 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (¬ ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅ → ¬ (C ∩ (◡R “ {D})) = ∅))
45	44	a3d 70	. 2 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → ((C ∩ (◡R “ {D})) = ∅ → ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅))
46	1	com12 13	. . . . . . . . . . . . . 14 ⊢ (x ∈ C → (C ⊆ A → x ∈ A))
47		funfvima 2904	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun H ∧ x ∈ dom H) → (x ∈ C → (H ‘x) ∈ (H “ C)))
48	47	funfni 2724	. . . . . . . . . . . . . . . 16 ⊢ ((H Fn A ∧ x ∈ A) → (x ∈ C → (H ‘x) ∈ (H “ C)))
49	48	exp 291	. . . . . . . . . . . . . . 15 ⊢ (H Fn A → (x ∈ A → (x ∈ C → (H ‘x) ∈ (H “ C))))
50	49	com13 33	. . . . . . . . . . . . . 14 ⊢ (x ∈ C → (x ∈ A → (H Fn A → (H ‘x) ∈ (H “ C))))
51	46, 50	syld 27	. . . . . . . . . . . . 13 ⊢ (x ∈ C → (C ⊆ A → (H Fn A → (H ‘x) ∈ (H “ C))))
52	51	com13 33	. . . . . . . . . . . 12 ⊢ (H Fn A → (C ⊆ A → (x ∈ C → (H ‘x) ∈ (H “ C))))
53	52	imp 277	. . . . . . . . . . 11 ⊢ ((H Fn A ∧ C ⊆ A) → (x ∈ C → (H ‘x) ∈ (H “ C)))
54	53	adantrr 312	. . . . . . . . . 10 ⊢ ((H Fn A ∧ (C ⊆ A ∧ D ∈ A)) → (x ∈ C → (H ‘x) ∈ (H “ C)))
55	2, 3	syl 12	. . . . . . . . . 10 ⊢ (H Isom R, S (A, B) → H Fn A)
56	54, 55	sylan 343	. . . . . . . . 9 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (x ∈ C → (H ‘x) ∈ (H “ C)))
57	56	adantrd 308	. . . . . . . 8 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → ((x ∈ C ∧ x ∈ (◡R “ {D})) → (H ‘x) ∈ (H “ C)))
58	25	biimpd 135	. . . . . . . . . . . . . . 15 ⊢ ((H Isom R, S (A, B) ∧ (x ∈ A ∧ D ∈ A)) → (xRD → (H ‘x)S(H ‘D)))
59		fvex 2838	. . . . . . . . . . . . . . . . 17 ⊢ (H ‘x) ∈ V
60	59	eliniseg 2618	. . . . . . . . . . . . . . . 16 ⊢ ((H ‘D) ∈ V → ((H ‘x) ∈ (◡S “ {(H ‘D)}) ↔ (H ‘x)S(H ‘D)))
61	13, 60	ax-mp 6	. . . . . . . . . . . . . . 15 ⊢ ((H ‘x) ∈ (◡S “ {(H ‘D)}) ↔ (H ‘x)S(H ‘D))
62	58, 61	syl6ibr 186	. . . . . . . . . . . . . 14 ⊢ ((H Isom R, S (A, B) ∧ (x ∈ A ∧ D ∈ A)) → (xRD → (H ‘x) ∈ (◡S “ {(H ‘D)})))
63	24, 62	sylbid 178	. . . . . . . . . . . . 13 ⊢ ((H Isom R, S (A, B) ∧ (x ∈ A ∧ D ∈ A)) → (x ∈ (◡R “ {D}) → (H ‘x) ∈ (◡S “ {(H ‘D)})))
64	63	exp32 294	. . . . . . . . . . . 12 ⊢ (H Isom R, S (A, B) → (x ∈ A → (D ∈ A → (x ∈ (◡R “ {D}) → (H ‘x) ∈ (◡S “ {(H ‘D)})))))
65	1, 64	syl9r 56	. . . . . . . . . . 11 ⊢ (H Isom R, S (A, B) → (C ⊆ A → (x ∈ C → (D ∈ A → (x ∈ (◡R “ {D}) → (H ‘x) ∈ (◡S “ {(H ‘D)}))))))
66	65	com34 36	. . . . . . . . . 10 ⊢ (H Isom R, S (A, B) → (C ⊆ A → (D ∈ A → (x ∈ C → (x ∈ (◡R “ {D}) → (H ‘x) ∈ (◡S “ {(H ‘D)}))))))
67	66	imp32 281	. . . . . . . . 9 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (x ∈ C → (x ∈ (◡R “ {D}) → (H ‘x) ∈ (◡S “ {(H ‘D)}))))
68	67	imp3a 279	. . . . . . . 8 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → ((x ∈ C ∧ x ∈ (◡R “ {D})) → (H ‘x) ∈ (◡S “ {(H ‘D)})))
69	57, 68	jcad 455	. . . . . . 7 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → ((x ∈ C ∧ x ∈ (◡R “ {D})) → ((H ‘x) ∈ (H “ C) ∧ (H ‘x) ∈ (◡S “ {(H ‘D)}))))
70		elin 1635	. . . . . . 7 ⊢ ((H ‘x) ∈ ((H “ C) ∩ (◡S “ {(H ‘D)})) ↔ ((H ‘x) ∈ (H “ C) ∧ (H ‘x) ∈ (◡S “ {(H ‘D)})))
71	69, 36, 70	3imtr4g 426	. . . . . 6 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (x ∈ (C ∩ (◡R “ {D})) → (H ‘x) ∈ ((H “ C) ∩ (◡S “ {(H ‘D)}))))
72		n0i 1712	. . . . . 6 ⊢ ((H ‘x) ∈ ((H “ C) ∩ (◡S “ {(H ‘D)})) → ¬ ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅)
73	71, 72	syl6 23	. . . . 5 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (x ∈ (C ∩ (◡R “ {D})) → ¬ ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅))
74	73	19.23adv 954	. . . 4 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (∃x x ∈ (C ∩ (◡R “ {D})) → ¬ ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅))
75	74, 38	syl5ib 181	. . 3 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (¬ (C ∩ (◡R “ {D})) = ∅ → ¬ ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅))
76	75	a3d 70	. 2 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → (((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅ → (C ∩ (◡R “ {D})) = ∅))
77	45, 76	impbid 397	1 ⊢ ((H Isom R, S (A, B) ∧ (C ⊆ A ∧ D ∈ A)) → ((C ∩ (◡R “ {D})) = ∅ ↔ ((H “ C) ∩ (◡S “ {(H ‘D)})) = ∅))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∃wex 678   = wceq 1091   ∈ wcel 1092  ∃wrex 1202  Vcvv 1348   ∩ cin 1486   ⊆ wss 1487  ∅c0 1707  {csn 1808   class class class wbr 2054  ^◡ccnv 2409   “ cima 2413   Fn wfn 2417  –1-1-onto→wf1o 2421   ‘cfv 2422   Isom wiso 2423

This theorem is referenced by:  isofrlem 2939

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-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-f1o 2437  df-fv 2438  df-iso 2439

metamath.org