ordiso2

Description: Generalize ordiso to proper classes. (Contributed by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Assertion	ordiso2	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to A = B$

Proof

Step	Hyp	Ref	Expression
1		ordsson	$⊢ Ord A \to A \subseteq On$
2	1	3ad2ant2	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to A \subseteq On$
3	2	sseld	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to x \in On)$
4		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
5		fveq2	$⊢ x = y \to F (x) = F (y)$
6		id	$⊢ x = y \to x = y$
7	5 6	eqeq12d	$⊢ x = y \to (F (x) = x \leftrightarrow F (y) = y)$
8	4 7	imbi12d	$⊢ x = y \to ((x \in A \to F (x) = x) \leftrightarrow (y \in A \to F (y) = y))$
9	8	imbi2d	$⊢ x = y \to (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to F (x) = x)) \leftrightarrow ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (y \in A \to F (y) = y)))$
10		r19.21v	$⊢ \forall y \in x ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (y \in A \to F (y) = y)) \leftrightarrow ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to \forall y \in x (y \in A \to F (y) = y))$
11		ordelss	$⊢ (Ord A \land x \in A) \to x \subseteq A$
12	11	3ad2antl2	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land x \in A) \to x \subseteq A$
13	12	sselda	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land x \in A) \land y \in x) \to y \in A$
14		pm5.5	$⊢ y \in A \to ((y \in A \to F (y) = y) \leftrightarrow F (y) = y)$
15	13 14	syl	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land x \in A) \land y \in x) \to ((y \in A \to F (y) = y) \leftrightarrow F (y) = y)$
16	15	ralbidva	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land x \in A) \to (\forall y \in x (y \in A \to F (y) = y) \leftrightarrow \forall y \in x F (y) = y)$
17		isof1o	$⊢ F {Isom}_{E, E} (A, B) \to F : A \underset{1-1 onto}{⟶} B$
18	17	3ad2ant1	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to F : A \underset{1-1 onto}{⟶} B$
19	18	ad2antrr	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F : A \underset{1-1 onto}{⟶} B$
20		simpll3	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to Ord B$
21		simpr	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to z \in F (x)$
22		f1of	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A ⟶ B$
23	17 22	syl	$⊢ F {Isom}_{E, E} (A, B) \to F : A ⟶ B$
24	23	3ad2ant1	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to F : A ⟶ B$
25	24	ad2antrr	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F : A ⟶ B$
26		simplrl	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to x \in A$
27	25 26	ffvelcdmd	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F (x) \in B$
28	21 27	jca	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to (z \in F (x) \land F (x) \in B)$
29		ordtr1	$⊢ Ord B \to ((z \in F (x) \land F (x) \in B) \to z \in B)$
30	20 28 29	sylc	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to z \in B$
31		f1ocnvfv2	$⊢ (F : A \underset{1-1 onto}{⟶} B \land z \in B) \to F (F^{-1} (z)) = z$
32	19 30 31	syl2anc	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F (F^{-1} (z)) = z$
33	32 21	eqeltrd	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F (F^{-1} (z)) \in F (x)$
34		simpll1	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F {Isom}_{E, E} (A, B)$
35		f1ocnv	$⊢ F : A \underset{1-1 onto}{⟶} B \to F^{-1} : B \underset{1-1 onto}{⟶} A$
36		f1of	$⊢ F^{-1} : B \underset{1-1 onto}{⟶} A \to F^{-1} : B ⟶ A$
37	19 35 36	3syl	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F^{-1} : B ⟶ A$
38	37 30	ffvelcdmd	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F^{-1} (z) \in A$
39		isorel	$⊢ (F {Isom}_{E, E} (A, B) \land (F^{-1} (z) \in A \land x \in A)) \to (F^{-1} (z) E x \leftrightarrow F (F^{-1} (z)) E F (x))$
40	34 38 26 39	syl12anc	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to (F^{-1} (z) E x \leftrightarrow F (F^{-1} (z)) E F (x))$
41		epel	$⊢ F^{-1} (z) E x \leftrightarrow F^{-1} (z) \in x$
42		fvex	$⊢ F (x) \in V$
43	42	epeli	$⊢ F (F^{-1} (z)) E F (x) \leftrightarrow F (F^{-1} (z)) \in F (x)$
44	40 41 43	3bitr3g	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to (F^{-1} (z) \in x \leftrightarrow F (F^{-1} (z)) \in F (x))$
45	33 44	mpbird	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F^{-1} (z) \in x$
46		simplrr	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to \forall y \in x F (y) = y$
47		fveq2	$⊢ y = F^{-1} (z) \to F (y) = F (F^{-1} (z))$
48		id	$⊢ y = F^{-1} (z) \to y = F^{-1} (z)$
49	47 48	eqeq12d	$⊢ y = F^{-1} (z) \to (F (y) = y \leftrightarrow F (F^{-1} (z)) = F^{-1} (z))$
50	49	rspcv	$⊢ F^{-1} (z) \in x \to (\forall y \in x F (y) = y \to F (F^{-1} (z)) = F^{-1} (z))$
51	45 46 50	sylc	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to F (F^{-1} (z)) = F^{-1} (z)$
52	32 51	eqtr3d	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to z = F^{-1} (z)$
53	52 45	eqeltrd	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in F (x)) \to z \in x$
54		simprr	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \to \forall y \in x F (y) = y$
55		fveq2	$⊢ y = z \to F (y) = F (z)$
56		id	$⊢ y = z \to y = z$
57	55 56	eqeq12d	$⊢ y = z \to (F (y) = y \leftrightarrow F (z) = z)$
58	57	rspccva	$⊢ (\forall y \in x F (y) = y \land z \in x) \to F (z) = z$
59	54 58	sylan	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in x) \to F (z) = z$
60		epel	$⊢ z E x \leftrightarrow z \in x$
61	60	bilanri	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in x) \to z E x$
62		simpll1	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in x) \to F {Isom}_{E, E} (A, B)$
63		simpl2	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \to Ord A$
64		simprl	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \to x \in A$
65	63 64 11	syl2anc	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \to x \subseteq A$
66	65	sselda	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in x) \to z \in A$
67		simplrl	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in x) \to x \in A$
68		isorel	$⊢ (F {Isom}_{E, E} (A, B) \land (z \in A \land x \in A)) \to (z E x \leftrightarrow F (z) E F (x))$
69	62 66 67 68	syl12anc	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in x) \to (z E x \leftrightarrow F (z) E F (x))$
70	61 69	mpbid	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in x) \to F (z) E F (x)$
71	42	epeli	$⊢ F (z) E F (x) \leftrightarrow F (z) \in F (x)$
72	70 71	sylib	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in x) \to F (z) \in F (x)$
73	59 72	eqeltrrd	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \land z \in x) \to z \in F (x)$
74	53 73	impbida	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \to (z \in F (x) \leftrightarrow z \in x)$
75	74	eqrdv	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land (x \in A \land \forall y \in x F (y) = y)) \to F (x) = x$
76	75	expr	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land x \in A) \to (\forall y \in x F (y) = y \to F (x) = x)$
77	16 76	sylbid	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land x \in A) \to (\forall y \in x (y \in A \to F (y) = y) \to F (x) = x)$
78	77	ex	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to (\forall y \in x (y \in A \to F (y) = y) \to F (x) = x))$
79	78	com23	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (\forall y \in x (y \in A \to F (y) = y) \to (x \in A \to F (x) = x))$
80	79	a2i	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to \forall y \in x (y \in A \to F (y) = y)) \to ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to F (x) = x))$
81	80	a1i	$⊢ x \in On \to (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to \forall y \in x (y \in A \to F (y) = y)) \to ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to F (x) = x)))$
82	10 81	biimtrid	$⊢ x \in On \to (\forall y \in x ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (y \in A \to F (y) = y)) \to ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to F (x) = x)))$
83	9 82	tfis2	$⊢ x \in On \to ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to F (x) = x))$
84	83	com3l	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to (x \in On \to F (x) = x))$
85	3 84	mpdd	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to F (x) = x)$
86	85	ralrimiv	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to \forall x \in A F (x) = x$
87		fveq2	$⊢ x = z \to F (x) = F (z)$
88		id	$⊢ x = z \to x = z$
89	87 88	eqeq12d	$⊢ x = z \to (F (x) = x \leftrightarrow F (z) = z)$
90	89	rspccva	$⊢ (\forall x \in A F (x) = x \land z \in A) \to F (z) = z$
91	90	adantll	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \land z \in A) \to F (z) = z$
92	23	ffvelcdmda	$⊢ (F {Isom}_{E, E} (A, B) \land z \in A) \to F (z) \in B$
93	92	3ad2antl1	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land z \in A) \to F (z) \in B$
94	93	adantlr	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \land z \in A) \to F (z) \in B$
95	91 94	eqeltrrd	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \land z \in A) \to z \in B$
96	95	ex	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to (z \in A \to z \in B)$
97		simpl1	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to F {Isom}_{E, E} (A, B)$
98		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{onto}{⟶} B$
99		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
100	17 98 99	3syl	$⊢ F {Isom}_{E, E} (A, B) \to ran F = B$
101	97 100	syl	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to ran F = B$
102	101	eleq2d	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to (z \in ran F \leftrightarrow z \in B)$
103		f1ofn	$⊢ F : A \underset{1-1 onto}{⟶} B \to F Fn A$
104	17 103	syl	$⊢ F {Isom}_{E, E} (A, B) \to F Fn A$
105	104	3ad2ant1	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to F Fn A$
106	105	adantr	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to F Fn A$
107		fvelrnb	$⊢ F Fn A \to (z \in ran F \leftrightarrow \exists w \in A F (w) = z)$
108	106 107	syl	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to (z \in ran F \leftrightarrow \exists w \in A F (w) = z)$
109	102 108	bitr3d	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to (z \in B \leftrightarrow \exists w \in A F (w) = z)$
110		fveq2	$⊢ x = w \to F (x) = F (w)$
111		id	$⊢ x = w \to x = w$
112	110 111	eqeq12d	$⊢ x = w \to (F (x) = x \leftrightarrow F (w) = w)$
113	112	rspcv	$⊢ w \in A \to (\forall x \in A F (x) = x \to F (w) = w)$
114	113	a1i	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (w \in A \to (\forall x \in A F (x) = x \to F (w) = w))$
115		simpr	$⊢ (F (w) = w \land F (w) = z) \to F (w) = z$
116		simpl	$⊢ (F (w) = w \land F (w) = z) \to F (w) = w$
117	115 116	eqtr3d	$⊢ (F (w) = w \land F (w) = z) \to z = w$
118	117	adantl	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land w \in A) \land (F (w) = w \land F (w) = z)) \to z = w$
119		simplr	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land w \in A) \land (F (w) = w \land F (w) = z)) \to w \in A$
120	118 119	eqeltrd	$⊢ (((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land w \in A) \land (F (w) = w \land F (w) = z)) \to z \in A$
121	120	exp43	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (w \in A \to (F (w) = w \to (F (w) = z \to z \in A)))$
122	114 121	syldd	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (w \in A \to (\forall x \in A F (x) = x \to (F (w) = z \to z \in A)))$
123	122	com23	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (\forall x \in A F (x) = x \to (w \in A \to (F (w) = z \to z \in A)))$
124	123	imp	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to (w \in A \to (F (w) = z \to z \in A))$
125	124	rexlimdv	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to (\exists w \in A F (w) = z \to z \in A)$
126	109 125	sylbid	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to (z \in B \to z \in A)$
127	96 126	impbid	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to (z \in A \leftrightarrow z \in B)$
128	127	eqrdv	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to A = B$
129	86 128	mpdan	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to A = B$

Metamath Proof Explorer

Theorem ordiso2

Proof