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	ffvelrnd	$⊢ (((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	ffvelrnd	$⊢ (((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	biimpri	$⊢ z \in x \to z E x$
62	61	adantl	$⊢ (((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$
63		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)$
64		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$
65		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$
66	64 65 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$
67	66	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$
68		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$
69		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))$
70	63 67 68 69	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))$
71	62 70	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)$
72	42	epeli	$⊢ F (z) E F (x) \leftrightarrow F (z) \in F (x)$
73	71 72	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)$
74	59 73	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)$
75	53 74	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)$
76	75	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$
77	76	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)$
78	16 77	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)$
79	78	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))$
80	79	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))$
81	80	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))$
82	81	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)))$
83	10 82	syl5bi	$⊢ 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)))$
84	9 83	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))$
85	84	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))$
86	3 85	mpdd	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to (x \in A \to F (x) = x)$
87	86	ralrimiv	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to \forall x \in A F (x) = x$
88		fveq2	$⊢ x = z \to F (x) = F (z)$
89		id	$⊢ x = z \to x = z$
90	88 89	eqeq12d	$⊢ x = z \to (F (x) = x \leftrightarrow F (z) = z)$
91	90	rspccva	$⊢ (\forall x \in A F (x) = x \land z \in A) \to F (z) = z$
92	91	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$
93	23	ffvelrnda	$⊢ (F {Isom}_{E, E} (A, B) \land z \in A) \to F (z) \in B$
94	93	3ad2antl1	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land z \in A) \to F (z) \in B$
95	94	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$
96	92 95	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$
97	96	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)$
98		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)$
99		f1ofo	$⊢ F : A \underset{1-1 onto}{⟶} B \to F : A \underset{onto}{⟶} B$
100		forn	$⊢ F : A \underset{onto}{⟶} B \to ran F = B$
101	17 99 100	3syl	$⊢ F {Isom}_{E, E} (A, B) \to ran F = B$
102	98 101	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$
103	102	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)$
104		f1ofn	$⊢ F : A \underset{1-1 onto}{⟶} B \to F Fn A$
105	17 104	syl	$⊢ F {Isom}_{E, E} (A, B) \to F Fn A$
106	105	3ad2ant1	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to F Fn A$
107	106	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$
108		fvelrnb	$⊢ F Fn A \to (z \in ran F \leftrightarrow \exists w \in A F (w) = z)$
109	107 108	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)$
110	103 109	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)$
111		fveq2	$⊢ x = w \to F (x) = F (w)$
112		id	$⊢ x = w \to x = w$
113	111 112	eqeq12d	$⊢ x = w \to (F (x) = x \leftrightarrow F (w) = w)$
114	113	rspcv	$⊢ w \in A \to (\forall x \in A F (x) = x \to F (w) = w)$
115	114	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))$
116		simpr	$⊢ (F (w) = w \land F (w) = z) \to F (w) = z$
117		simpl	$⊢ (F (w) = w \land F (w) = z) \to F (w) = w$
118	116 117	eqtr3d	$⊢ (F (w) = w \land F (w) = z) \to z = w$
119	118	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$
120		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$
121	119 120	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$
122	121	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)))$
123	115 122	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)))$
124	123	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)))$
125	124	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))$
126	125	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)$
127	110 126	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)$
128	97 127	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)$
129	128	eqrdv	$⊢ ((F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \land \forall x \in A F (x) = x) \to A = B$
130	87 129	mpdan	$⊢ (F {Isom}_{E, E} (A, B) \land Ord A \land Ord B) \to A = B$

Metamath Proof Explorer

Theorem ordiso2

Proof