Metamath Proof Explorer

Theorem dfac12lem2

Description: Lemma for dfac12 . (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Hypotheses dfac12.1 
|- ( ph -> A e. On )
dfac12.3 
|- ( ph -> F : ~P ( har ` ( R1 ` A ) ) -1-1-> On )
dfac12.4 
|- G = recs ( ( x e. _V |-> ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) )
dfac12.5 
|- ( ph -> C e. On )
dfac12.h 
|- H = ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) )
dfac12.6 
|- ( ph -> C C_ A )
dfac12.8 
|- ( ph -> A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On )
Assertion dfac12lem2 
|- ( ph -> ( G ` C ) : ( R1 ` C ) -1-1-> On )

Proof

Step Hyp Ref Expression
1 dfac12.1 
 |-  ( ph -> A e. On )
2 dfac12.3 
 |-  ( ph -> F : ~P ( har ` ( R1 ` A ) ) -1-1-> On )
3 dfac12.4 
 |-  G = recs ( ( x e. _V |-> ( y e. ( R1 ` dom x ) |-> if ( dom x = U. dom x , ( ( suc U. ran U. ran x .o ( rank ` y ) ) +o ( ( x ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( ( `' OrdIso ( _E , ran ( x ` U. dom x ) ) o. ( x ` U. dom x ) ) " y ) ) ) ) ) )
4 dfac12.5 
 |-  ( ph -> C e. On )
5 dfac12.h 
 |-  H = ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) )
6 dfac12.6 
 |-  ( ph -> C C_ A )
7 dfac12.8 
 |-  ( ph -> A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On )
8 3 tfr1 
 |-  G Fn On
9 fnfun 
 |-  ( G Fn On -> Fun G )
10 8 9 ax-mp 
 |-  Fun G
11 funimaexg 
 |-  ( ( Fun G /\ C e. On ) -> ( G " C ) e. _V )
12 10 4 11 sylancr 
 |-  ( ph -> ( G " C ) e. _V )
13 uniexg 
 |-  ( ( G " C ) e. _V -> U. ( G " C ) e. _V )
14 rnexg 
 |-  ( U. ( G " C ) e. _V -> ran U. ( G " C ) e. _V )
15 12 13 14 3syl 
 |-  ( ph -> ran U. ( G " C ) e. _V )
16 f1f 
 |-  ( ( G ` z ) : ( R1 ` z ) -1-1-> On -> ( G ` z ) : ( R1 ` z ) --> On )
17 fssxp 
 |-  ( ( G ` z ) : ( R1 ` z ) --> On -> ( G ` z ) C_ ( ( R1 ` z ) X. On ) )
18 ssv 
 |-  ( R1 ` z ) C_ _V
19 xpss1 
 |-  ( ( R1 ` z ) C_ _V -> ( ( R1 ` z ) X. On ) C_ ( _V X. On ) )
20 18 19 ax-mp 
 |-  ( ( R1 ` z ) X. On ) C_ ( _V X. On )
21 sstr 
 |-  ( ( ( G ` z ) C_ ( ( R1 ` z ) X. On ) /\ ( ( R1 ` z ) X. On ) C_ ( _V X. On ) ) -> ( G ` z ) C_ ( _V X. On ) )
22 20 21 mpan2 
 |-  ( ( G ` z ) C_ ( ( R1 ` z ) X. On ) -> ( G ` z ) C_ ( _V X. On ) )
23 fvex 
 |-  ( G ` z ) e. _V
24 23 elpw 
 |-  ( ( G ` z ) e. ~P ( _V X. On ) <-> ( G ` z ) C_ ( _V X. On ) )
25 22 24 sylibr 
 |-  ( ( G ` z ) C_ ( ( R1 ` z ) X. On ) -> ( G ` z ) e. ~P ( _V X. On ) )
26 16 17 25 3syl 
 |-  ( ( G ` z ) : ( R1 ` z ) -1-1-> On -> ( G ` z ) e. ~P ( _V X. On ) )
27 26 ralimi 
 |-  ( A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On -> A. z e. C ( G ` z ) e. ~P ( _V X. On ) )
28 7 27 syl 
 |-  ( ph -> A. z e. C ( G ` z ) e. ~P ( _V X. On ) )
29 onss 
 |-  ( C e. On -> C C_ On )
30 4 29 syl 
 |-  ( ph -> C C_ On )
31 8 fndmi 
 |-  dom G = On
32 30 31 sseqtrrdi 
 |-  ( ph -> C C_ dom G )
33 funimass4 
 |-  ( ( Fun G /\ C C_ dom G ) -> ( ( G " C ) C_ ~P ( _V X. On ) <-> A. z e. C ( G ` z ) e. ~P ( _V X. On ) ) )
34 10 32 33 sylancr 
 |-  ( ph -> ( ( G " C ) C_ ~P ( _V X. On ) <-> A. z e. C ( G ` z ) e. ~P ( _V X. On ) ) )
35 28 34 mpbird 
 |-  ( ph -> ( G " C ) C_ ~P ( _V X. On ) )
36 sspwuni 
 |-  ( ( G " C ) C_ ~P ( _V X. On ) <-> U. ( G " C ) C_ ( _V X. On ) )
37 35 36 sylib 
 |-  ( ph -> U. ( G " C ) C_ ( _V X. On ) )
38 rnss 
 |-  ( U. ( G " C ) C_ ( _V X. On ) -> ran U. ( G " C ) C_ ran ( _V X. On ) )
39 37 38 syl 
 |-  ( ph -> ran U. ( G " C ) C_ ran ( _V X. On ) )
40 rnxpss 
 |-  ran ( _V X. On ) C_ On
41 39 40 sstrdi 
 |-  ( ph -> ran U. ( G " C ) C_ On )
42 ssonuni 
 |-  ( ran U. ( G " C ) e. _V -> ( ran U. ( G " C ) C_ On -> U. ran U. ( G " C ) e. On ) )
43 15 41 42 sylc 
 |-  ( ph -> U. ran U. ( G " C ) e. On )
44 onsuc 
 |-  ( U. ran U. ( G " C ) e. On -> suc U. ran U. ( G " C ) e. On )
45 43 44 syl 
 |-  ( ph -> suc U. ran U. ( G " C ) e. On )
46 45 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> suc U. ran U. ( G " C ) e. On )
47 rankon 
 |-  ( rank ` y ) e. On
48 omcl 
 |-  ( ( suc U. ran U. ( G " C ) e. On /\ ( rank ` y ) e. On ) -> ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) e. On )
49 46 47 48 sylancl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) e. On )
50 fveq2 
 |-  ( z = suc ( rank ` y ) -> ( G ` z ) = ( G ` suc ( rank ` y ) ) )
51 f1eq1 
 |-  ( ( G ` z ) = ( G ` suc ( rank ` y ) ) -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` z ) -1-1-> On ) )
52 50 51 syl 
 |-  ( z = suc ( rank ` y ) -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` z ) -1-1-> On ) )
53 fveq2 
 |-  ( z = suc ( rank ` y ) -> ( R1 ` z ) = ( R1 ` suc ( rank ` y ) ) )
54 f1eq2 
 |-  ( ( R1 ` z ) = ( R1 ` suc ( rank ` y ) ) -> ( ( G ` suc ( rank ` y ) ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On ) )
55 53 54 syl 
 |-  ( z = suc ( rank ` y ) -> ( ( G ` suc ( rank ` y ) ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On ) )
56 52 55 bitrd 
 |-  ( z = suc ( rank ` y ) -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On ) )
57 7 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On )
58 rankr1ai 
 |-  ( y e. ( R1 ` C ) -> ( rank ` y ) e. C )
59 58 ad2antlr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( rank ` y ) e. C )
60 simpr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> C = U. C )
61 59 60 eleqtrd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( rank ` y ) e. U. C )
62 eloni 
 |-  ( C e. On -> Ord C )
63 4 62 syl 
 |-  ( ph -> Ord C )
64 63 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> Ord C )
65 ordsucuniel 
 |-  ( Ord C -> ( ( rank ` y ) e. U. C <-> suc ( rank ` y ) e. C ) )
66 64 65 syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( rank ` y ) e. U. C <-> suc ( rank ` y ) e. C ) )
67 61 66 mpbid 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> suc ( rank ` y ) e. C )
68 56 57 67 rspcdva 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On )
69 f1f 
 |-  ( ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) --> On )
70 68 69 syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) --> On )
71 r1elwf 
 |-  ( y e. ( R1 ` C ) -> y e. U. ( R1 " On ) )
72 71 ad2antlr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> y e. U. ( R1 " On ) )
73 rankidb 
 |-  ( y e. U. ( R1 " On ) -> y e. ( R1 ` suc ( rank ` y ) ) )
74 72 73 syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> y e. ( R1 ` suc ( rank ` y ) ) )
75 70 74 ffvelcdmd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. On )
76 oacl 
 |-  ( ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) e. On /\ ( ( G ` suc ( rank ` y ) ) ` y ) e. On ) -> ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) e. On )
77 49 75 76 syl2anc 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) e. On )
78 f1f 
 |-  ( F : ~P ( har ` ( R1 ` A ) ) -1-1-> On -> F : ~P ( har ` ( R1 ` A ) ) --> On )
79 2 78 syl 
 |-  ( ph -> F : ~P ( har ` ( R1 ` A ) ) --> On )
80 79 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> F : ~P ( har ` ( R1 ` A ) ) --> On )
81 imassrn 
 |-  ( H " y ) C_ ran H
82 fvex 
 |-  ( G ` U. C ) e. _V
83 82 rnex 
 |-  ran ( G ` U. C ) e. _V
84 fveq2 
 |-  ( z = U. C -> ( G ` z ) = ( G ` U. C ) )
85 f1eq1 
 |-  ( ( G ` z ) = ( G ` U. C ) -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` z ) -1-1-> On ) )
86 84 85 syl 
 |-  ( z = U. C -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` z ) -1-1-> On ) )
87 fveq2 
 |-  ( z = U. C -> ( R1 ` z ) = ( R1 ` U. C ) )
88 f1eq2 
 |-  ( ( R1 ` z ) = ( R1 ` U. C ) -> ( ( G ` U. C ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On ) )
89 87 88 syl 
 |-  ( z = U. C -> ( ( G ` U. C ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On ) )
90 86 89 bitrd 
 |-  ( z = U. C -> ( ( G ` z ) : ( R1 ` z ) -1-1-> On <-> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On ) )
91 7 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> A. z e. C ( G ` z ) : ( R1 ` z ) -1-1-> On )
92 4 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> C e. On )
93 onuni 
 |-  ( C e. On -> U. C e. On )
94 sucidg 
 |-  ( U. C e. On -> U. C e. suc U. C )
95 92 93 94 3syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> U. C e. suc U. C )
96 63 adantr 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> Ord C )
97 orduniorsuc 
 |-  ( Ord C -> ( C = U. C \/ C = suc U. C ) )
98 96 97 syl 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> ( C = U. C \/ C = suc U. C ) )
99 98 orcanai 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> C = suc U. C )
100 95 99 eleqtrrd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> U. C e. C )
101 90 91 100 rspcdva 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On )
102 f1f 
 |-  ( ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On -> ( G ` U. C ) : ( R1 ` U. C ) --> On )
103 frn 
 |-  ( ( G ` U. C ) : ( R1 ` U. C ) --> On -> ran ( G ` U. C ) C_ On )
104 101 102 103 3syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran ( G ` U. C ) C_ On )
105 epweon 
 |-  _E We On
106 wess 
 |-  ( ran ( G ` U. C ) C_ On -> ( _E We On -> _E We ran ( G ` U. C ) ) )
107 104 105 106 mpisyl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> _E We ran ( G ` U. C ) )
108 eqid 
 |-  OrdIso ( _E , ran ( G ` U. C ) ) = OrdIso ( _E , ran ( G ` U. C ) )
109 108 oiiso 
 |-  ( ( ran ( G ` U. C ) e. _V /\ _E We ran ( G ` U. C ) ) -> OrdIso ( _E , ran ( G ` U. C ) ) Isom _E , _E ( dom OrdIso ( _E , ran ( G ` U. C ) ) , ran ( G ` U. C ) ) )
110 83 107 109 sylancr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> OrdIso ( _E , ran ( G ` U. C ) ) Isom _E , _E ( dom OrdIso ( _E , ran ( G ` U. C ) ) , ran ( G ` U. C ) ) )
111 isof1o 
 |-  ( OrdIso ( _E , ran ( G ` U. C ) ) Isom _E , _E ( dom OrdIso ( _E , ran ( G ` U. C ) ) , ran ( G ` U. C ) ) -> OrdIso ( _E , ran ( G ` U. C ) ) : dom OrdIso ( _E , ran ( G ` U. C ) ) -1-1-onto-> ran ( G ` U. C ) )
112 f1ocnv 
 |-  ( OrdIso ( _E , ran ( G ` U. C ) ) : dom OrdIso ( _E , ran ( G ` U. C ) ) -1-1-onto-> ran ( G ` U. C ) -> `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-onto-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
113 f1of1 
 |-  ( `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-onto-> dom OrdIso ( _E , ran ( G ` U. C ) ) -> `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
114 110 111 112 113 4syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
115 f1f1orn 
 |-  ( ( G ` U. C ) : ( R1 ` U. C ) -1-1-> On -> ( G ` U. C ) : ( R1 ` U. C ) -1-1-onto-> ran ( G ` U. C ) )
116 f1of1 
 |-  ( ( G ` U. C ) : ( R1 ` U. C ) -1-1-onto-> ran ( G ` U. C ) -> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> ran ( G ` U. C ) )
117 101 115 116 3syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( G ` U. C ) : ( R1 ` U. C ) -1-1-> ran ( G ` U. C ) )
118 f1co 
 |-  ( ( `' OrdIso ( _E , ran ( G ` U. C ) ) : ran ( G ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) /\ ( G ` U. C ) : ( R1 ` U. C ) -1-1-> ran ( G ` U. C ) ) -> ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
119 114 117 118 syl2anc 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
120 f1eq1 
 |-  ( H = ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) -> ( H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) <-> ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) ) )
121 5 120 ax-mp 
 |-  ( H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) <-> ( `' OrdIso ( _E , ran ( G ` U. C ) ) o. ( G ` U. C ) ) : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
122 119 121 sylibr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
123 f1f 
 |-  ( H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) -> H : ( R1 ` U. C ) --> dom OrdIso ( _E , ran ( G ` U. C ) ) )
124 frn 
 |-  ( H : ( R1 ` U. C ) --> dom OrdIso ( _E , ran ( G ` U. C ) ) -> ran H C_ dom OrdIso ( _E , ran ( G ` U. C ) ) )
125 122 123 124 3syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran H C_ dom OrdIso ( _E , ran ( G ` U. C ) ) )
126 harcl 
 |-  ( har ` ( R1 ` A ) ) e. On
127 126 onordi 
 |-  Ord ( har ` ( R1 ` A ) )
128 108 oion 
 |-  ( ran ( G ` U. C ) e. _V -> dom OrdIso ( _E , ran ( G ` U. C ) ) e. On )
129 83 128 mp1i 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) e. On )
130 108 oien 
 |-  ( ( ran ( G ` U. C ) e. _V /\ _E We ran ( G ` U. C ) ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) ~~ ran ( G ` U. C ) )
131 83 107 130 sylancr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) ~~ ran ( G ` U. C ) )
132 fvex 
 |-  ( R1 ` U. C ) e. _V
133 132 f1oen 
 |-  ( ( G ` U. C ) : ( R1 ` U. C ) -1-1-onto-> ran ( G ` U. C ) -> ( R1 ` U. C ) ~~ ran ( G ` U. C ) )
134 ensym 
 |-  ( ( R1 ` U. C ) ~~ ran ( G ` U. C ) -> ran ( G ` U. C ) ~~ ( R1 ` U. C ) )
135 101 115 133 134 4syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran ( G ` U. C ) ~~ ( R1 ` U. C ) )
136 fvex 
 |-  ( R1 ` A ) e. _V
137 1 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> A e. On )
138 6 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> C C_ A )
139 138 100 sseldd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> U. C e. A )
140 r1ord2 
 |-  ( A e. On -> ( U. C e. A -> ( R1 ` U. C ) C_ ( R1 ` A ) ) )
141 137 139 140 sylc 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` U. C ) C_ ( R1 ` A ) )
142 ssdomg 
 |-  ( ( R1 ` A ) e. _V -> ( ( R1 ` U. C ) C_ ( R1 ` A ) -> ( R1 ` U. C ) ~<_ ( R1 ` A ) ) )
143 136 141 142 mpsyl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` U. C ) ~<_ ( R1 ` A ) )
144 endomtr 
 |-  ( ( ran ( G ` U. C ) ~~ ( R1 ` U. C ) /\ ( R1 ` U. C ) ~<_ ( R1 ` A ) ) -> ran ( G ` U. C ) ~<_ ( R1 ` A ) )
145 135 143 144 syl2anc 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran ( G ` U. C ) ~<_ ( R1 ` A ) )
146 endomtr 
 |-  ( ( dom OrdIso ( _E , ran ( G ` U. C ) ) ~~ ran ( G ` U. C ) /\ ran ( G ` U. C ) ~<_ ( R1 ` A ) ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) ~<_ ( R1 ` A ) )
147 131 145 146 syl2anc 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) ~<_ ( R1 ` A ) )
148 elharval 
 |-  ( dom OrdIso ( _E , ran ( G ` U. C ) ) e. ( har ` ( R1 ` A ) ) <-> ( dom OrdIso ( _E , ran ( G ` U. C ) ) e. On /\ dom OrdIso ( _E , ran ( G ` U. C ) ) ~<_ ( R1 ` A ) ) )
149 129 147 148 sylanbrc 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) e. ( har ` ( R1 ` A ) ) )
150 ordelss 
 |-  ( ( Ord ( har ` ( R1 ` A ) ) /\ dom OrdIso ( _E , ran ( G ` U. C ) ) e. ( har ` ( R1 ` A ) ) ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) C_ ( har ` ( R1 ` A ) ) )
151 127 149 150 sylancr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> dom OrdIso ( _E , ran ( G ` U. C ) ) C_ ( har ` ( R1 ` A ) ) )
152 125 151 sstrd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ran H C_ ( har ` ( R1 ` A ) ) )
153 81 152 sstrid 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " y ) C_ ( har ` ( R1 ` A ) ) )
154 fvex 
 |-  ( har ` ( R1 ` A ) ) e. _V
155 154 elpw2 
 |-  ( ( H " y ) e. ~P ( har ` ( R1 ` A ) ) <-> ( H " y ) C_ ( har ` ( R1 ` A ) ) )
156 153 155 sylibr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " y ) e. ~P ( har ` ( R1 ` A ) ) )
157 80 156 ffvelcdmd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( F ` ( H " y ) ) e. On )
158 77 157 ifclda 
 |-  ( ( ph /\ y e. ( R1 ` C ) ) -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) e. On )
159 158 ex 
 |-  ( ph -> ( y e. ( R1 ` C ) -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) e. On ) )
160 iftrue 
 |-  ( C = U. C -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) )
161 iftrue 
 |-  ( C = U. C -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) )
162 160 161 eqeq12d 
 |-  ( C = U. C -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) ) )
163 162 adantl 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) ) )
164 45 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> suc U. ran U. ( G " C ) e. On )
165 nsuceq0 
 |-  suc U. ran U. ( G " C ) =/= (/)
166 165 a1i 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> suc U. ran U. ( G " C ) =/= (/) )
167 47 a1i 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( rank ` y ) e. On )
168 onsucuni 
 |-  ( ran U. ( G " C ) C_ On -> ran U. ( G " C ) C_ suc U. ran U. ( G " C ) )
169 41 168 syl 
 |-  ( ph -> ran U. ( G " C ) C_ suc U. ran U. ( G " C ) )
170 169 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ran U. ( G " C ) C_ suc U. ran U. ( G " C ) )
171 30 ad2antrr 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> C C_ On )
172 fnfvima 
 |-  ( ( G Fn On /\ C C_ On /\ suc ( rank ` y ) e. C ) -> ( G ` suc ( rank ` y ) ) e. ( G " C ) )
173 8 171 67 172 mp3an2i 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) e. ( G " C ) )
174 elssuni 
 |-  ( ( G ` suc ( rank ` y ) ) e. ( G " C ) -> ( G ` suc ( rank ` y ) ) C_ U. ( G " C ) )
175 rnss 
 |-  ( ( G ` suc ( rank ` y ) ) C_ U. ( G " C ) -> ran ( G ` suc ( rank ` y ) ) C_ ran U. ( G " C ) )
176 173 174 175 3syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ran ( G ` suc ( rank ` y ) ) C_ ran U. ( G " C ) )
177 f1fn 
 |-  ( ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On -> ( G ` suc ( rank ` y ) ) Fn ( R1 ` suc ( rank ` y ) ) )
178 68 177 syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) Fn ( R1 ` suc ( rank ` y ) ) )
179 fnfvelrn 
 |-  ( ( ( G ` suc ( rank ` y ) ) Fn ( R1 ` suc ( rank ` y ) ) /\ y e. ( R1 ` suc ( rank ` y ) ) ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. ran ( G ` suc ( rank ` y ) ) )
180 178 74 179 syl2anc 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. ran ( G ` suc ( rank ` y ) ) )
181 176 180 sseldd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. ran U. ( G " C ) )
182 170 181 sseldd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) )
183 182 adantlrr 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) )
184 rankon 
 |-  ( rank ` z ) e. On
185 184 a1i 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( rank ` z ) e. On )
186 eleq1w 
 |-  ( y = z -> ( y e. ( R1 ` C ) <-> z e. ( R1 ` C ) ) )
187 186 anbi2d 
 |-  ( y = z -> ( ( ph /\ y e. ( R1 ` C ) ) <-> ( ph /\ z e. ( R1 ` C ) ) ) )
188 187 anbi1d 
 |-  ( y = z -> ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) <-> ( ( ph /\ z e. ( R1 ` C ) ) /\ C = U. C ) ) )
189 fveq2 
 |-  ( y = z -> ( rank ` y ) = ( rank ` z ) )
190 suceq 
 |-  ( ( rank ` y ) = ( rank ` z ) -> suc ( rank ` y ) = suc ( rank ` z ) )
191 189 190 syl 
 |-  ( y = z -> suc ( rank ` y ) = suc ( rank ` z ) )
192 191 fveq2d 
 |-  ( y = z -> ( G ` suc ( rank ` y ) ) = ( G ` suc ( rank ` z ) ) )
193 id 
 |-  ( y = z -> y = z )
194 192 193 fveq12d 
 |-  ( y = z -> ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) )
195 194 eleq1d 
 |-  ( y = z -> ( ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) <-> ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) ) )
196 188 195 imbi12d 
 |-  ( y = z -> ( ( ( ( ph /\ y e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) ) <-> ( ( ( ph /\ z e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) ) ) )
197 196 182 chvarvv 
 |-  ( ( ( ph /\ z e. ( R1 ` C ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) )
198 197 adantlrl 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) )
199 omopth2 
 |-  ( ( ( suc U. ran U. ( G " C ) e. On /\ suc U. ran U. ( G " C ) =/= (/) ) /\ ( ( rank ` y ) e. On /\ ( ( G ` suc ( rank ` y ) ) ` y ) e. suc U. ran U. ( G " C ) ) /\ ( ( rank ` z ) e. On /\ ( ( G ` suc ( rank ` z ) ) ` z ) e. suc U. ran U. ( G " C ) ) ) -> ( ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) <-> ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) ) )
200 164 166 167 183 185 198 199 syl222anc 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) = ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) <-> ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) ) )
201 190 adantl 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> suc ( rank ` y ) = suc ( rank ` z ) )
202 201 fveq2d 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( G ` suc ( rank ` y ) ) = ( G ` suc ( rank ` z ) ) )
203 202 fveq1d 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( G ` suc ( rank ` y ) ) ` z ) = ( ( G ` suc ( rank ` z ) ) ` z ) )
204 203 eqeq2d 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` y ) ) ` z ) <-> ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) )
205 68 adantlrr 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On )
206 205 adantr 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On )
207 74 adantlrr 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> y e. ( R1 ` suc ( rank ` y ) ) )
208 207 adantr 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> y e. ( R1 ` suc ( rank ` y ) ) )
209 r1elwf 
 |-  ( z e. ( R1 ` C ) -> z e. U. ( R1 " On ) )
210 rankidb 
 |-  ( z e. U. ( R1 " On ) -> z e. ( R1 ` suc ( rank ` z ) ) )
211 209 210 syl 
 |-  ( z e. ( R1 ` C ) -> z e. ( R1 ` suc ( rank ` z ) ) )
212 211 ad2antll 
 |-  ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) -> z e. ( R1 ` suc ( rank ` z ) ) )
213 212 ad2antrr 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> z e. ( R1 ` suc ( rank ` z ) ) )
214 201 fveq2d 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( R1 ` suc ( rank ` y ) ) = ( R1 ` suc ( rank ` z ) ) )
215 213 214 eleqtrrd 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> z e. ( R1 ` suc ( rank ` y ) ) )
216 f1fveq 
 |-  ( ( ( G ` suc ( rank ` y ) ) : ( R1 ` suc ( rank ` y ) ) -1-1-> On /\ ( y e. ( R1 ` suc ( rank ` y ) ) /\ z e. ( R1 ` suc ( rank ` y ) ) ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` y ) ) ` z ) <-> y = z ) )
217 206 208 215 216 syl12anc 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` y ) ) ` z ) <-> y = z ) )
218 204 217 bitr3d 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) <-> y = z ) )
219 218 biimpd 
 |-  ( ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) /\ ( rank ` y ) = ( rank ` z ) ) -> ( ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) -> y = z ) )
220 219 expimpd 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) -> y = z ) )
221 189 194 jca 
 |-  ( y = z -> ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) )
222 220 221 impbid1 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( ( ( rank ` y ) = ( rank ` z ) /\ ( ( G ` suc ( rank ` y ) ) ` y ) = ( ( G ` suc ( rank ` z ) ) ` z ) ) <-> y = z ) )
223 163 200 222 3bitrd 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ C = U. C ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> y = z ) )
224 iffalse 
 |-  ( -. C = U. C -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = ( F ` ( H " y ) ) )
225 iffalse 
 |-  ( -. C = U. C -> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) = ( F ` ( H " z ) ) )
226 224 225 eqeq12d 
 |-  ( -. C = U. C -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> ( F ` ( H " y ) ) = ( F ` ( H " z ) ) ) )
227 226 adantl 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> ( F ` ( H " y ) ) = ( F ` ( H " z ) ) ) )
228 2 ad2antrr 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> F : ~P ( har ` ( R1 ` A ) ) -1-1-> On )
229 156 adantlrr 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( H " y ) e. ~P ( har ` ( R1 ` A ) ) )
230 187 anbi1d 
 |-  ( y = z -> ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) <-> ( ( ph /\ z e. ( R1 ` C ) ) /\ -. C = U. C ) ) )
231 imaeq2 
 |-  ( y = z -> ( H " y ) = ( H " z ) )
232 231 eleq1d 
 |-  ( y = z -> ( ( H " y ) e. ~P ( har ` ( R1 ` A ) ) <-> ( H " z ) e. ~P ( har ` ( R1 ` A ) ) ) )
233 230 232 imbi12d 
 |-  ( y = z -> ( ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " y ) e. ~P ( har ` ( R1 ` A ) ) ) <-> ( ( ( ph /\ z e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " z ) e. ~P ( har ` ( R1 ` A ) ) ) ) )
234 233 156 chvarvv 
 |-  ( ( ( ph /\ z e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( H " z ) e. ~P ( har ` ( R1 ` A ) ) )
235 234 adantlrl 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( H " z ) e. ~P ( har ` ( R1 ` A ) ) )
236 f1fveq 
 |-  ( ( F : ~P ( har ` ( R1 ` A ) ) -1-1-> On /\ ( ( H " y ) e. ~P ( har ` ( R1 ` A ) ) /\ ( H " z ) e. ~P ( har ` ( R1 ` A ) ) ) ) -> ( ( F ` ( H " y ) ) = ( F ` ( H " z ) ) <-> ( H " y ) = ( H " z ) ) )
237 228 229 235 236 syl12anc 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( ( F ` ( H " y ) ) = ( F ` ( H " z ) ) <-> ( H " y ) = ( H " z ) ) )
238 122 adantlrr 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) )
239 simplrl 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> y e. ( R1 ` C ) )
240 99 fveq2d 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` C ) = ( R1 ` suc U. C ) )
241 r1suc 
 |-  ( U. C e. On -> ( R1 ` suc U. C ) = ~P ( R1 ` U. C ) )
242 92 93 241 3syl 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` suc U. C ) = ~P ( R1 ` U. C ) )
243 240 242 eqtrd 
 |-  ( ( ( ph /\ y e. ( R1 ` C ) ) /\ -. C = U. C ) -> ( R1 ` C ) = ~P ( R1 ` U. C ) )
244 243 adantlrr 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( R1 ` C ) = ~P ( R1 ` U. C ) )
245 239 244 eleqtrd 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> y e. ~P ( R1 ` U. C ) )
246 245 elpwid 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> y C_ ( R1 ` U. C ) )
247 simplrr 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> z e. ( R1 ` C ) )
248 247 244 eleqtrd 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> z e. ~P ( R1 ` U. C ) )
249 248 elpwid 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> z C_ ( R1 ` U. C ) )
250 f1imaeq 
 |-  ( ( H : ( R1 ` U. C ) -1-1-> dom OrdIso ( _E , ran ( G ` U. C ) ) /\ ( y C_ ( R1 ` U. C ) /\ z C_ ( R1 ` U. C ) ) ) -> ( ( H " y ) = ( H " z ) <-> y = z ) )
251 238 246 249 250 syl12anc 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( ( H " y ) = ( H " z ) <-> y = z ) )
252 227 237 251 3bitrd 
 |-  ( ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) /\ -. C = U. C ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> y = z ) )
253 223 252 pm2.61dan 
 |-  ( ( ph /\ ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> y = z ) )
254 253 ex 
 |-  ( ph -> ( ( y e. ( R1 ` C ) /\ z e. ( R1 ` C ) ) -> ( if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) = if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` z ) ) +o ( ( G ` suc ( rank ` z ) ) ` z ) ) , ( F ` ( H " z ) ) ) <-> y = z ) ) )
255 159 254 dom2lem 
 |-  ( ph -> ( y e. ( R1 ` C ) |-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) : ( R1 ` C ) -1-1-> On )
256 1 2 3 4 5 dfac12lem1 
 |-  ( ph -> ( G ` C ) = ( y e. ( R1 ` C ) |-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) )
257 f1eq1 
 |-  ( ( G ` C ) = ( y e. ( R1 ` C ) |-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) -> ( ( G ` C ) : ( R1 ` C ) -1-1-> On <-> ( y e. ( R1 ` C ) |-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) : ( R1 ` C ) -1-1-> On ) )
258 256 257 syl 
 |-  ( ph -> ( ( G ` C ) : ( R1 ` C ) -1-1-> On <-> ( y e. ( R1 ` C ) |-> if ( C = U. C , ( ( suc U. ran U. ( G " C ) .o ( rank ` y ) ) +o ( ( G ` suc ( rank ` y ) ) ` y ) ) , ( F ` ( H " y ) ) ) ) : ( R1 ` C ) -1-1-> On ) )
259 255 258 mpbird 
 |-  ( ph -> ( G ` C ) : ( R1 ` C ) -1-1-> On )