Metamath Proof Explorer


Theorem ordiso2

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

Ref Expression
Assertion ordiso2 F Isom E , E A B Ord A Ord B A = B

Proof

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