This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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