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 biimpri 
 |-  ( z e. x -> z _E x )
62 61 adantl 
 |-  ( ( ( ( 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 )
63 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 ) )
64 simpl2 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) -> Ord A )
65 simprl 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) -> x e. A )
66 64 65 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 )
67 66 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 )
68 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 )
69 isorel 
 |-  ( ( F Isom _E , _E ( A , B ) /\ ( z e. A /\ x e. 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 e. A /\ A. y e. x ( F ` y ) = y ) ) /\ z e. x ) -> ( z _E x <-> ( F ` z ) _E ( F ` x ) ) )
71 62 70 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 ) )
72 42 epeli 
 |-  ( ( F ` z ) _E ( F ` x ) <-> ( F ` z ) e. ( F ` x ) )
73 71 72 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 ) )
74 59 73 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 ) )
75 53 74 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 ) )
76 75 eqrdv 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ ( x e. A /\ A. y e. x ( F ` y ) = y ) ) -> ( F ` x ) = x )
77 76 expr 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ x e. A ) -> ( A. y e. x ( F ` y ) = y -> ( F ` x ) = x ) )
78 16 77 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 ) )
79 78 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 ) ) )
80 79 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 ) ) )
81 80 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 ) ) )
82 81 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 ) ) ) )
83 10 82 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 ) ) ) )
84 9 83 tfis2 
 |-  ( x e. On -> ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( F ` x ) = x ) ) )
85 84 com3l 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( x e. On -> ( F ` x ) = x ) ) )
86 3 85 mpdd 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( x e. A -> ( F ` x ) = x ) )
87 86 ralrimiv 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A. x e. 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 
 |-  ( ( A. x e. A ( F ` x ) = x /\ z e. A ) -> ( F ` z ) = z )
92 91 adantll 
 |-  ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) /\ z e. A ) -> ( F ` z ) = z )
93 23 ffvelcdmda 
 |-  ( ( F Isom _E , _E ( A , B ) /\ z e. A ) -> ( F ` z ) e. B )
94 93 3ad2antl1 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ z e. A ) -> ( F ` z ) e. B )
95 94 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 )
96 92 95 eqeltrrd 
 |-  ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) /\ z e. A ) -> z e. B )
97 96 ex 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( z e. A -> z e. B ) )
98 simpl1 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. 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 ) /\ A. x e. A ( F ` x ) = x ) -> ran F = B )
103 102 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 ) )
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 ) /\ A. x e. A ( F ` x ) = x ) -> F Fn A )
108 fvelrnb 
 |-  ( F Fn A -> ( z e. ran F <-> E. w e. A ( F ` w ) = z ) )
109 107 108 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 ) )
110 103 109 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 ) )
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 e. A -> ( A. x e. A ( F ` x ) = x -> ( F ` w ) = w ) )
115 114 a1i 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( w e. A -> ( A. x e. 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 e. A ) /\ ( ( F ` w ) = w /\ ( F ` w ) = z ) ) -> z = w )
120 simplr 
 |-  ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ w e. A ) /\ ( ( F ` w ) = w /\ ( F ` w ) = z ) ) -> w e. A )
121 119 120 eqeltrd 
 |-  ( ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ w e. A ) /\ ( ( F ` w ) = w /\ ( F ` w ) = z ) ) -> z e. A )
122 121 exp43 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> ( w e. A -> ( ( F ` w ) = w -> ( ( F ` w ) = z -> z e. A ) ) ) )
123 115 122 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 ) ) ) )
124 123 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 ) ) ) )
125 124 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 ) ) )
126 125 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 ) )
127 110 126 sylbid 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( z e. B -> z e. A ) )
128 97 127 impbid 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> ( z e. A <-> z e. B ) )
129 128 eqrdv 
 |-  ( ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) /\ A. x e. A ( F ` x ) = x ) -> A = B )
130 87 129 mpdan 
 |-  ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ Ord B ) -> A = B )