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 suceloni
 |-  ( 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 ffvelrnd
 |-  ( ( ( 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 ffvelrnd
 |-  ( ( ( 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 )