MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac12lem2 Structured version   Unicode version

Theorem dfac12lem2 8305
Description: Lemma for dfac12 8310. (Contributed by Mario Carneiro, 29-May-2015.)
Hypotheses
Ref Expression
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
Ref Expression
dfac12lem2  |-  ( ph  ->  ( G `  C
) : ( R1
`  C ) -1-1-> On )
Distinct variable groups:    y, z, A    x, y, z, C   
x, G, y, z    ph, y, z    x, F, y, z    y, H, z
Allowed substitution hints:    ph( x)    A( x)    H( x)

Proof of Theorem dfac12lem2
StepHypRef Expression
1 dfac12.4 . . . . . . . . . . . . . 14  |-  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 ) ) ) ) ) )
21tfr1 6848 . . . . . . . . . . . . 13  |-  G  Fn  On
3 fnfun 5503 . . . . . . . . . . . . 13  |-  ( G  Fn  On  ->  Fun  G )
42, 3ax-mp 5 . . . . . . . . . . . 12  |-  Fun  G
5 dfac12.5 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  On )
6 funimaexg 5490 . . . . . . . . . . . 12  |-  ( ( Fun  G  /\  C  e.  On )  ->  ( G " C )  e. 
_V )
74, 5, 6sylancr 663 . . . . . . . . . . 11  |-  ( ph  ->  ( G " C
)  e.  _V )
8 uniexg 6372 . . . . . . . . . . 11  |-  ( ( G " C )  e.  _V  ->  U. ( G " C )  e. 
_V )
9 rnexg 6505 . . . . . . . . . . 11  |-  ( U. ( G " C )  e.  _V  ->  ran  U. ( G " C
)  e.  _V )
107, 8, 93syl 20 . . . . . . . . . 10  |-  ( ph  ->  ran  U. ( G
" C )  e. 
_V )
11 dfac12.8 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. z  e.  C  ( G `  z ) : ( R1 `  z ) -1-1-> On )
12 f1f 5601 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) : ( R1 `  z ) -1-1-> On  ->  ( G `  z ) : ( R1 `  z ) --> On )
13 fssxp 5565 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) : ( R1 `  z ) --> On  ->  ( G `  z ) 
C_  ( ( R1
`  z )  X.  On ) )
14 ssv 3371 . . . . . . . . . . . . . . . . . . . 20  |-  ( R1
`  z )  C_  _V
15 xpss1 4943 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R1 `  z ) 
C_  _V  ->  ( ( R1 `  z )  X.  On )  C_  ( _V  X.  On ) )
1614, 15ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( ( R1 `  z )  X.  On )  C_  ( _V  X.  On )
17 sstr 3359 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( G `  z
)  C_  ( ( R1 `  z )  X.  On )  /\  (
( R1 `  z
)  X.  On ) 
C_  ( _V  X.  On ) )  ->  ( G `  z )  C_  ( _V  X.  On ) )
1816, 17mpan2 671 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  z ) 
C_  ( ( R1
`  z )  X.  On )  ->  ( G `  z )  C_  ( _V  X.  On ) )
19 fvex 5696 . . . . . . . . . . . . . . . . . . 19  |-  ( G `
 z )  e. 
_V
2019elpw 3861 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  z )  e.  ~P ( _V 
X.  On )  <->  ( G `  z )  C_  ( _V  X.  On ) )
2118, 20sylibr 212 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) 
C_  ( ( R1
`  z )  X.  On )  ->  ( G `  z )  e.  ~P ( _V  X.  On ) )
2212, 13, 213syl 20 . . . . . . . . . . . . . . . 16  |-  ( ( G `  z ) : ( R1 `  z ) -1-1-> On  ->  ( G `  z )  e.  ~P ( _V 
X.  On ) )
2322ralimi 2786 . . . . . . . . . . . . . . 15  |-  ( A. z  e.  C  ( G `  z ) : ( R1 `  z ) -1-1-> On  ->  A. z  e.  C  ( G `  z )  e.  ~P ( _V 
X.  On ) )
2411, 23syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. z  e.  C  ( G `  z )  e.  ~P ( _V 
X.  On ) )
25 onss 6397 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  On  ->  C  C_  On )
265, 25syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  C_  On )
27 fndm 5505 . . . . . . . . . . . . . . . . 17  |-  ( G  Fn  On  ->  dom  G  =  On )
282, 27ax-mp 5 . . . . . . . . . . . . . . . 16  |-  dom  G  =  On
2926, 28syl6sseqr 3398 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  C_  dom  G )
30 funimass4 5737 . . . . . . . . . . . . . . 15  |-  ( ( Fun  G  /\  C  C_ 
dom  G )  -> 
( ( G " C )  C_  ~P ( _V  X.  On ) 
<-> 
A. z  e.  C  ( G `  z )  e.  ~P ( _V 
X.  On ) ) )
314, 29, 30sylancr 663 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( G " C )  C_  ~P ( _V  X.  On ) 
<-> 
A. z  e.  C  ( G `  z )  e.  ~P ( _V 
X.  On ) ) )
3224, 31mpbird 232 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G " C
)  C_  ~P ( _V  X.  On ) )
33 sspwuni 4251 . . . . . . . . . . . . 13  |-  ( ( G " C ) 
C_  ~P ( _V  X.  On )  <->  U. ( G " C )  C_  ( _V  X.  On ) )
3432, 33sylib 196 . . . . . . . . . . . 12  |-  ( ph  ->  U. ( G " C )  C_  ( _V  X.  On ) )
35 rnss 5063 . . . . . . . . . . . 12  |-  ( U. ( G " C ) 
C_  ( _V  X.  On )  ->  ran  U. ( G " C ) 
C_  ran  ( _V  X.  On ) )
3634, 35syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ran  U. ( G
" C )  C_  ran  ( _V  X.  On ) )
37 rnxpss 5265 . . . . . . . . . . 11  |-  ran  ( _V  X.  On )  C_  On
3836, 37syl6ss 3363 . . . . . . . . . 10  |-  ( ph  ->  ran  U. ( G
" C )  C_  On )
39 ssonuni 6393 . . . . . . . . . 10  |-  ( ran  U. ( G " C
)  e.  _V  ->  ( ran  U. ( G
" C )  C_  On  ->  U. ran  U. ( G " C )  e.  On ) )
4010, 38, 39sylc 60 . . . . . . . . 9  |-  ( ph  ->  U. ran  U. ( G " C )  e.  On )
41 suceloni 6419 . . . . . . . . 9  |-  ( U. ran  U. ( G " C )  e.  On  ->  suc  U. ran  U. ( G " C )  e.  On )
4240, 41syl 16 . . . . . . . 8  |-  ( ph  ->  suc  U. ran  U. ( G " C )  e.  On )
4342ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  suc  U. ran  U. ( G " C )  e.  On )
44 rankon 7994 . . . . . . 7  |-  ( rank `  y )  e.  On
45 omcl 6968 . . . . . . 7  |-  ( ( suc  U. ran  U. ( G " C )  e.  On  /\  ( rank `  y )  e.  On )  ->  ( suc  U. ran  U. ( G " C )  .o  ( rank `  y
) )  e.  On )
4643, 44, 45sylancl 662 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( suc  U. ran  U. ( G " C )  .o  ( rank `  y
) )  e.  On )
47 rankr1ai 7997 . . . . . . . . . . . 12  |-  ( y  e.  ( R1 `  C )  ->  ( rank `  y )  e.  C )
4847ad2antlr 726 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( rank `  y )  e.  C )
49 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  C  =  U. C )
5048, 49eleqtrd 2514 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( rank `  y )  e.  U. C )
51 eloni 4724 . . . . . . . . . . . . 13  |-  ( C  e.  On  ->  Ord  C )
525, 51syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  C )
5352ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  Ord  C )
54 ordsucuniel 6430 . . . . . . . . . . 11  |-  ( Ord 
C  ->  ( ( rank `  y )  e. 
U. C  <->  suc  ( rank `  y )  e.  C
) )
5553, 54syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( rank `  y
)  e.  U. C  <->  suc  ( rank `  y
)  e.  C ) )
5650, 55mpbid 210 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  suc  ( rank `  y
)  e.  C )
5711ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  A. z  e.  C  ( G `  z ) : ( R1 `  z ) -1-1-> On )
58 fveq2 5686 . . . . . . . . . . . 12  |-  ( z  =  suc  ( rank `  y )  ->  ( G `  z )  =  ( G `  suc  ( rank `  y
) ) )
59 f1eq1 5596 . . . . . . . . . . . 12  |-  ( ( G `  z )  =  ( G `  suc  ( rank `  y
) )  ->  (
( G `  z
) : ( R1
`  z ) -1-1-> On  <->  ( G `  suc  ( rank `  y ) ) : ( R1 `  z ) -1-1-> On ) )
6058, 59syl 16 . . . . . . . . . . 11  |-  ( z  =  suc  ( rank `  y )  ->  (
( G `  z
) : ( R1
`  z ) -1-1-> On  <->  ( G `  suc  ( rank `  y ) ) : ( R1 `  z ) -1-1-> On ) )
61 fveq2 5686 . . . . . . . . . . . 12  |-  ( z  =  suc  ( rank `  y )  ->  ( R1 `  z )  =  ( R1 `  suc  ( rank `  y )
) )
62 f1eq2 5597 . . . . . . . . . . . 12  |-  ( ( 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 ) )
6361, 62syl 16 . . . . . . . . . . 11  |-  ( z  =  suc  ( rank `  y )  ->  (
( G `  suc  ( rank `  y )
) : ( R1
`  z ) -1-1-> On  <->  ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y
) ) -1-1-> On ) )
6460, 63bitrd 253 . . . . . . . . . 10  |-  ( z  =  suc  ( rank `  y )  ->  (
( G `  z
) : ( R1
`  z ) -1-1-> On  <->  ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y
) ) -1-1-> On ) )
6564rspcv 3064 . . . . . . . . 9  |-  ( suc  ( rank `  y
)  e.  C  -> 
( A. z  e.  C  ( G `  z ) : ( R1 `  z )
-1-1-> On  ->  ( G `  suc  ( rank `  y
) ) : ( R1 `  suc  ( rank `  y ) )
-1-1-> On ) )
6656, 57, 65sylc 60 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
) : ( R1
`  suc  ( rank `  y ) ) -1-1-> On )
67 f1f 5601 . . . . . . . 8  |-  ( ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y
) ) -1-1-> On  ->  ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y
) ) --> On )
6866, 67syl 16 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
) : ( R1
`  suc  ( rank `  y ) ) --> On )
69 r1elwf 7995 . . . . . . . . 9  |-  ( y  e.  ( R1 `  C )  ->  y  e.  U. ( R1 " On ) )
7069ad2antlr 726 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
y  e.  U. ( R1 " On ) )
71 rankidb 7999 . . . . . . . 8  |-  ( y  e.  U. ( R1
" On )  -> 
y  e.  ( R1
`  suc  ( rank `  y ) ) )
7270, 71syl 16 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
y  e.  ( R1
`  suc  ( rank `  y ) ) )
7368, 72ffvelrnd 5839 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  On )
74 oacl 6967 . . . . . 6  |-  ( ( ( 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 )
7546, 73, 74syl2anc 661 . . . . 5  |-  ( ( ( 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 )
76 dfac12.3 . . . . . . . 8  |-  ( ph  ->  F : ~P (har `  ( R1 `  A
) ) -1-1-> On )
77 f1f 5601 . . . . . . . 8  |-  ( F : ~P (har `  ( R1 `  A ) ) -1-1-> On  ->  F : ~P (har `  ( R1 `  A ) ) --> On )
7876, 77syl 16 . . . . . . 7  |-  ( ph  ->  F : ~P (har `  ( R1 `  A
) ) --> On )
7978ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  F : ~P (har `  ( R1 `  A ) ) --> On )
80 imassrn 5175 . . . . . . . 8  |-  ( H
" y )  C_  ran  H
81 fvex 5696 . . . . . . . . . . . . . . 15  |-  ( G `
 U. C )  e.  _V
8281rnex 6507 . . . . . . . . . . . . . 14  |-  ran  ( G `  U. C )  e.  _V
835ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  C  e.  On )
84 onuni 6399 . . . . . . . . . . . . . . . . . . 19  |-  ( C  e.  On  ->  U. C  e.  On )
85 sucidg 4792 . . . . . . . . . . . . . . . . . . 19  |-  ( U. C  e.  On  ->  U. C  e.  suc  U. C )
8683, 84, 853syl 20 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  U. C  e.  suc  U. C )
8752adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  ( R1 `  C ) )  ->  Ord  C )
88 orduniorsuc 6436 . . . . . . . . . . . . . . . . . . . 20  |-  ( Ord 
C  ->  ( C  =  U. C  \/  C  =  suc  U. C ) )
8987, 88syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  ( R1 `  C ) )  ->  ( C  =  U. C  \/  C  =  suc  U. C ) )
9089orcanai 904 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  C  =  suc  U. C )
9186, 90eleqtrrd 2515 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  U. C  e.  C
)
9211ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  A. z  e.  C  ( G `  z ) : ( R1 `  z ) -1-1-> On )
93 fveq2 5686 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  U. C  -> 
( G `  z
)  =  ( G `
 U. C ) )
94 f1eq1 5596 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( G `  z )  =  ( G `  U. C )  ->  (
( G `  z
) : ( R1
`  z ) -1-1-> On  <->  ( G `  U. C
) : ( R1
`  z ) -1-1-> On ) )
9593, 94syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  U. C  -> 
( ( G `  z ) : ( R1 `  z )
-1-1-> On  <->  ( G `  U. C ) : ( R1 `  z )
-1-1-> On ) )
96 fveq2 5686 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  U. C  -> 
( R1 `  z
)  =  ( R1
`  U. C ) )
97 f1eq2 5597 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( R1 `  z )  =  ( R1 `  U. C )  ->  (
( G `  U. C ) : ( R1 `  z )
-1-1-> On  <->  ( G `  U. C ) : ( R1 `  U. C
) -1-1-> On ) )
9896, 97syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  U. C  -> 
( ( G `  U. C ) : ( R1 `  z )
-1-1-> On  <->  ( G `  U. C ) : ( R1 `  U. C
) -1-1-> On ) )
9995, 98bitrd 253 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  U. C  -> 
( ( G `  z ) : ( R1 `  z )
-1-1-> On  <->  ( G `  U. C ) : ( R1 `  U. C
) -1-1-> On ) )
10099rspcv 3064 . . . . . . . . . . . . . . . . 17  |-  ( U. C  e.  C  ->  ( A. z  e.  C  ( G `  z ) : ( R1 `  z ) -1-1-> On  ->  ( G `  U. C
) : ( R1
`  U. C ) -1-1-> On ) )
10191, 92, 100sylc 60 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( G `  U. C ) : ( R1 `  U. C
) -1-1-> On )
102 f1f 5601 . . . . . . . . . . . . . . . 16  |-  ( ( G `  U. C
) : ( R1
`  U. C ) -1-1-> On  ->  ( G `  U. C ) : ( R1 `  U. C
) --> On )
103 frn 5560 . . . . . . . . . . . . . . . 16  |-  ( ( G `  U. C
) : ( R1
`  U. C ) --> On 
->  ran  ( G `  U. C )  C_  On )
104101, 102, 1033syl 20 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  ( G `  U. C )  C_  On )
105 epweon 6390 . . . . . . . . . . . . . . 15  |-  _E  We  On
106 wess 4702 . . . . . . . . . . . . . . 15  |-  ( ran  ( G `  U. C )  C_  On  ->  (  _E  We  On  ->  _E  We  ran  ( G `  U. C ) ) )
107104, 105, 106mpisyl 18 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  _E  We  ran  ( G `  U. C
) )
108 eqid 2438 . . . . . . . . . . . . . . 15  |- OrdIso (  _E  ,  ran  ( G `
 U. C ) )  = OrdIso (  _E  ,  ran  ( G `
 U. C ) )
109108oiiso 7743 . . . . . . . . . . . . . 14  |-  ( ( 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
) ) )
11082, 107, 109sylancr 663 . . . . . . . . . . . . 13  |-  ( ( ( 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 6011 . . . . . . . . . . . . 13  |-  (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 5648 . . . . . . . . . . . . 13  |-  (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 5635 . . . . . . . . . . . . 13  |-  ( `'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 ) ) )
114110, 111, 112, 1134syl 21 . . . . . . . . . . . 12  |-  ( ( ( 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 5647 . . . . . . . . . . . . 13  |-  ( ( G `  U. C
) : ( R1
`  U. C ) -1-1-> On  ->  ( G `  U. C ) : ( R1 `  U. C
)
-1-1-onto-> ran  ( G `  U. C ) )
116 f1of1 5635 . . . . . . . . . . . . 13  |-  ( ( 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 ) )
117101, 115, 1163syl 20 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( G `  U. C ) : ( R1 `  U. C
) -1-1-> ran  ( G `  U. C ) )
118 f1co 5610 . . . . . . . . . . . 12  |-  ( ( `'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 ) ) )
119114, 117, 118syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( 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 dfac12.h . . . . . . . . . . . 12  |-  H  =  ( `'OrdIso (  _E  ,  ran  ( G `
 U. C ) )  o.  ( G `
 U. C ) )
121 f1eq1 5596 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
122120, 121ax-mp 5 . . . . . . . . . . 11  |-  ( 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 ) ) )
123119, 122sylibr 212 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  H : ( R1 `  U. C
) -1-1-> dom OrdIso (  _E  ,  ran  ( G `  U. C ) ) )
124 f1f 5601 . . . . . . . . . 10  |-  ( H : ( R1 `  U. C ) -1-1-> dom OrdIso (  _E  ,  ran  ( G `
 U. C ) )  ->  H :
( R1 `  U. C ) --> dom OrdIso (  _E  ,  ran  ( G `
 U. C ) ) )
125 frn 5560 . . . . . . . . . 10  |-  ( H : ( R1 `  U. C ) --> dom OrdIso (  _E  ,  ran  ( G `
 U. C ) )  ->  ran  H  C_  dom OrdIso (  _E  ,  ran  ( G `  U. C
) ) )
126123, 124, 1253syl 20 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  H  C_  dom OrdIso (  _E  ,  ran  ( G `  U. C ) ) )
127 harcl 7768 . . . . . . . . . . 11  |-  (har `  ( R1 `  A ) )  e.  On
128127onordi 4818 . . . . . . . . . 10  |-  Ord  (har `  ( R1 `  A
) )
129108oion 7742 . . . . . . . . . . . 12  |-  ( ran  ( G `  U. C )  e.  _V  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  e.  On )
13082, 129mp1i 12 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  e.  On )
131108oien 7744 . . . . . . . . . . . . 13  |-  ( ( ran  ( G `  U. C )  e.  _V  /\  _E  We  ran  ( G `  U. C ) )  ->  dom OrdIso (  _E  ,  ran  ( G `
 U. C ) )  ~~  ran  ( G `  U. C ) )
13282, 107, 131sylancr 663 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  ~~  ran  ( G `  U. C ) )
133 fvex 5696 . . . . . . . . . . . . . . 15  |-  ( R1
`  U. C )  e. 
_V
134133f1oen 7322 . . . . . . . . . . . . . 14  |-  ( ( G `  U. C
) : ( R1
`  U. C ) -1-1-onto-> ran  ( G `  U. C )  ->  ( R1 `  U. C )  ~~  ran  ( G `  U. C
) )
135 ensym 7350 . . . . . . . . . . . . . 14  |-  ( ( R1 `  U. C
)  ~~  ran  ( G `
 U. C )  ->  ran  ( G `  U. C )  ~~  ( R1 `  U. C
) )
136101, 115, 134, 1354syl 21 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  ( G `  U. C )  ~~  ( R1 `  U. C
) )
137 fvex 5696 . . . . . . . . . . . . . 14  |-  ( R1
`  A )  e. 
_V
138 dfac12.1 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  On )
139138ad2antrr 725 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  A  e.  On )
140 dfac12.6 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  C  C_  A )
141140ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  C  C_  A
)
142141, 91sseldd 3352 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  U. C  e.  A
)
143 r1ord2 7980 . . . . . . . . . . . . . . 15  |-  ( A  e.  On  ->  ( U. C  e.  A  ->  ( R1 `  U. C )  C_  ( R1 `  A ) ) )
144139, 142, 143sylc 60 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  U. C )  C_  ( R1 `  A ) )
145 ssdomg 7347 . . . . . . . . . . . . . 14  |-  ( ( R1 `  A )  e.  _V  ->  (
( R1 `  U. C )  C_  ( R1 `  A )  -> 
( R1 `  U. C )  ~<_  ( R1
`  A ) ) )
146137, 144, 145mpsyl 63 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  U. C )  ~<_  ( R1
`  A ) )
147 endomtr 7359 . . . . . . . . . . . . 13  |-  ( ( ran  ( G `  U. C )  ~~  ( R1 `  U. C )  /\  ( R1 `  U. C )  ~<_  ( R1
`  A ) )  ->  ran  ( G `  U. C )  ~<_  ( R1 `  A ) )
148136, 146, 147syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  ( G `  U. C )  ~<_  ( R1 `  A ) )
149 endomtr 7359 . . . . . . . . . . . 12  |-  ( ( 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 ) )
150132, 148, 149syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  ~<_  ( R1 `  A ) )
151 elharval 7770 . . . . . . . . . . 11  |-  ( 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 ) ) )
152130, 150, 151sylanbrc 664 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  e.  (har `  ( R1 `  A ) ) )
153 ordelss 4730 . . . . . . . . . 10  |-  ( ( 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 ) ) )
154128, 152, 153sylancr 663 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  C_  (har `  ( R1 `  A ) ) )
155126, 154sstrd 3361 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  H  C_  (har `  ( R1 `  A
) ) )
15680, 155syl5ss 3362 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( H "
y )  C_  (har `  ( R1 `  A
) ) )
157 fvex 5696 . . . . . . . 8  |-  (har `  ( R1 `  A ) )  e.  _V
158157elpw2 4451 . . . . . . 7  |-  ( ( H " y )  e.  ~P (har `  ( R1 `  A ) )  <->  ( H "
y )  C_  (har `  ( R1 `  A
) ) )
159156, 158sylibr 212 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( H "
y )  e.  ~P (har `  ( R1 `  A ) ) )
16079, 159ffvelrnd 5839 . . . . 5  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( F `  ( H " y ) )  e.  On )
16175, 160ifclda 3816 . . . 4  |-  ( (
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 )
162161ex 434 . . 3  |-  ( 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 ) )
163 iftrue 3792 . . . . . . . 8  |-  ( 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 )
) )
164 iftrue 3792 . . . . . . . 8  |-  ( 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 )
) )
165163, 164eqeq12d 2452 . . . . . . 7  |-  ( 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 ) ) ) )
166165adantl 466 . . . . . 6  |-  ( ( ( 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 )
) ) )
16742ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  suc  U.
ran  U. ( G " C )  e.  On )
168 nsuceq0 4794 . . . . . . . 8  |-  suc  U. ran  U. ( G " C )  =/=  (/)
169168a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  suc  U.
ran  U. ( G " C )  =/=  (/) )
17044a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  ( rank `  y )  e.  On )
171 onsucuni 6434 . . . . . . . . . . 11  |-  ( ran  U. ( G " C
)  C_  On  ->  ran  U. ( G " C
)  C_  suc  U. ran  U. ( G " C
) )
17238, 171syl 16 . . . . . . . . . 10  |-  ( ph  ->  ran  U. ( G
" C )  C_  suc  U. ran  U. ( G " C ) )
173172ad2antrr 725 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  ran  U. ( G " C )  C_  suc  U.
ran  U. ( G " C ) )
1742a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  G  Fn  On )
17526ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  C  C_  On )
176 fnfvima 5950 . . . . . . . . . . . 12  |-  ( ( G  Fn  On  /\  C  C_  On  /\  suc  ( rank `  y )  e.  C )  ->  ( G `  suc  ( rank `  y ) )  e.  ( G " C
) )
177174, 175, 56, 176syl3anc 1218 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
)  e.  ( G
" C ) )
178 elssuni 4116 . . . . . . . . . . 11  |-  ( ( G `  suc  ( rank `  y ) )  e.  ( G " C )  ->  ( G `  suc  ( rank `  y ) )  C_  U. ( G " C
) )
179 rnss 5063 . . . . . . . . . . 11  |-  ( ( G `  suc  ( rank `  y ) ) 
C_  U. ( G " C )  ->  ran  ( G `  suc  ( rank `  y ) ) 
C_  ran  U. ( G " C ) )
180177, 178, 1793syl 20 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  ran  ( G `  suc  ( rank `  y )
)  C_  ran  U. ( G " C ) )
181 f1fn 5602 . . . . . . . . . . . 12  |-  ( ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y
) ) -1-1-> On  ->  ( G `  suc  ( rank `  y ) )  Fn  ( R1 `  suc  ( rank `  y
) ) )
18266, 181syl 16 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
)  Fn  ( R1
`  suc  ( rank `  y ) ) )
183 fnfvelrn 5835 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
184182, 72, 183syl2anc 661 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  ran  ( G `  suc  ( rank `  y ) ) )
185180, 184sseldd 3352 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  ran  U. ( G " C ) )
186173, 185sseldd 3352 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  suc  U. ran  U. ( G " C ) )
187186adantlrr 720 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  (
( G `  suc  ( rank `  y )
) `  y )  e.  suc  U. ran  U. ( G " C ) )
188 rankon 7994 . . . . . . . 8  |-  ( rank `  z )  e.  On
189188a1i 11 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  ( rank `  z )  e.  On )
190 eleq1 2498 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y  e.  ( R1
`  C )  <->  z  e.  ( R1 `  C ) ) )
191190anbi2d 703 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( ph  /\  y  e.  ( R1 `  C
) )  <->  ( ph  /\  z  e.  ( R1
`  C ) ) ) )
192191anbi1d 704 . . . . . . . . . 10  |-  ( y  =  z  ->  (
( ( ph  /\  y  e.  ( R1 `  C ) )  /\  C  =  U. C )  <-> 
( ( ph  /\  z  e.  ( R1 `  C ) )  /\  C  =  U. C ) ) )
193 fveq2 5686 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  ( rank `  y )  =  ( rank `  z
) )
194 suceq 4779 . . . . . . . . . . . . . 14  |-  ( (
rank `  y )  =  ( rank `  z
)  ->  suc  ( rank `  y )  =  suc  ( rank `  z )
)
195193, 194syl 16 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  suc  ( rank `  y )  =  suc  ( rank `  z
) )
196195fveq2d 5690 . . . . . . . . . . . 12  |-  ( y  =  z  ->  ( G `  suc  ( rank `  y ) )  =  ( G `  suc  ( rank `  z )
) )
197 id 22 . . . . . . . . . . . 12  |-  ( y  =  z  ->  y  =  z )
198196, 197fveq12d 5692 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( G `  suc  ( rank `  y )
) `  y )  =  ( ( G `
 suc  ( rank `  z ) ) `  z ) )
199198eleq1d 2504 . . . . . . . . . 10  |-  ( 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 ) ) )
200192, 199imbi12d 320 . . . . . . . . 9  |-  ( 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 ) ) ) )
201200, 186chvarv 1958 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  z
) ) `  z
)  e.  suc  U. ran  U. ( G " C ) )
202201adantlrl 719 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  (
( G `  suc  ( rank `  z )
) `  z )  e.  suc  U. ran  U. ( G " C ) )
203 omopth2 7015 . . . . . . 7  |-  ( ( ( 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 ) ) ) )
204167, 169, 170, 187, 189, 202, 203syl222anc 1234 . . . . . 6  |-  ( ( ( 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 )
) ) )
205194adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  suc  ( rank `  y )  =  suc  ( rank `  z
) )
206205fveq2d 5690 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  ( G `  suc  ( rank `  y ) )  =  ( G `  suc  ( rank `  z )
) )
207206fveq1d 5688 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) )
208207eqeq2d 2449 . . . . . . . . . 10  |-  ( ( ( ( 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 )
) )
20966adantlrr 720 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y )
) -1-1-> On )
210209adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( 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 )
21172adantlrr 720 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  y  e.  ( R1 `  suc  ( rank `  y )
) )
212211adantr 465 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  y  e.  ( R1 `  suc  ( rank `  y )
) )
213 r1elwf 7995 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( R1 `  C )  ->  z  e.  U. ( R1 " On ) )
214 rankidb 7999 . . . . . . . . . . . . . . 15  |-  ( z  e.  U. ( R1
" On )  -> 
z  e.  ( R1
`  suc  ( rank `  z ) ) )
215213, 214syl 16 . . . . . . . . . . . . . 14  |-  ( z  e.  ( R1 `  C )  ->  z  e.  ( R1 `  suc  ( rank `  z )
) )
216215ad2antll 728 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  ( R1 `  C
)  /\  z  e.  ( R1 `  C ) ) )  ->  z  e.  ( R1 `  suc  ( rank `  z )
) )
217216ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  z  e.  ( R1 `  suc  ( rank `  z )
) )
218205fveq2d 5690 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  ( R1 `  suc  ( rank `  y ) )  =  ( R1 `  suc  ( rank `  z )
) )
219217, 218eleqtrrd 2515 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  z  e.  ( R1 `  suc  ( rank `  y )
) )
220 f1fveq 5970 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
221210, 212, 219, 220syl12anc 1216 . . . . . . . . . 10  |-  ( ( ( ( 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 ) )
222208, 221bitr3d 255 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
223222biimpd 207 . . . . . . . 8  |-  ( ( ( ( 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 ) )
224223expimpd 603 . . . . . . 7  |-  ( ( ( 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 ) )
225193, 198jca 532 . . . . . . 7  |-  ( y  =  z  ->  (
( rank `  y )  =  ( rank `  z
)  /\  ( ( G `  suc  ( rank `  y ) ) `  y )  =  ( ( G `  suc  ( rank `  z )
) `  z )
) )
226224, 225impbid1 203 . . . . . 6  |-  ( ( ( 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 ) )
227166, 204, 2263bitrd 279 . . . . 5  |-  ( ( ( 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 ) )
228 iffalse 3794 . . . . . . . 8  |-  ( -.  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 ) ) )
229 iffalse 3794 . . . . . . . 8  |-  ( -.  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 ) ) )
230228, 229eqeq12d 2452 . . . . . . 7  |-  ( -.  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 ) ) ) )
231230adantl 466 . . . . . 6  |-  ( ( ( 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 ) ) ) )
23276ad2antrr 725 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  ->  F : ~P (har `  ( R1 `  A ) ) -1-1-> On )
233159adantlrr 720 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( H " y
)  e.  ~P (har `  ( R1 `  A
) ) )
234191anbi1d 704 . . . . . . . . . 10  |-  ( y  =  z  ->  (
( ( ph  /\  y  e.  ( R1 `  C ) )  /\  -.  C  =  U. C )  <->  ( ( ph  /\  z  e.  ( R1 `  C ) )  /\  -.  C  =  U. C ) ) )
235 imaeq2 5160 . . . . . . . . . . 11  |-  ( y  =  z  ->  ( H " y )  =  ( H " z
) )
236235eleq1d 2504 . . . . . . . . . 10  |-  ( y  =  z  ->  (
( H " y
)  e.  ~P (har `  ( R1 `  A
) )  <->  ( H " z )  e.  ~P (har `  ( R1 `  A ) ) ) )
237234, 236imbi12d 320 . . . . . . . . 9  |-  ( 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 ) ) ) ) )
238237, 159chvarv 1958 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( H "
z )  e.  ~P (har `  ( R1 `  A ) ) )
239238adantlrl 719 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( H " z
)  e.  ~P (har `  ( R1 `  A
) ) )
240 f1fveq 5970 . . . . . . 7  |-  ( ( 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 ) ) )
241232, 233, 239, 240syl12anc 1216 . . . . . 6  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( ( F `  ( H " y ) )  =  ( F `
 ( H "
z ) )  <->  ( H " y )  =  ( H " z ) ) )
242123adantlrr 720 . . . . . . 7  |-  ( ( ( 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 ) ) )
243 simplrl 759 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
y  e.  ( R1
`  C ) )
24490fveq2d 5690 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  C )  =  ( R1 `  suc  U. C ) )
245 r1suc 7969 . . . . . . . . . . . 12  |-  ( U. C  e.  On  ->  ( R1 `  suc  U. C )  =  ~P ( R1 `  U. C
) )
24683, 84, 2453syl 20 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  suc  U. C )  =  ~P ( R1 `  U. C ) )
247244, 246eqtrd 2470 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  C )  =  ~P ( R1 `  U. C
) )
248247adantlrr 720 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( R1 `  C
)  =  ~P ( R1 `  U. C ) )
249243, 248eleqtrd 2514 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
y  e.  ~P ( R1 `  U. C ) )
250249elpwid 3865 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
y  C_  ( R1 ` 
U. C ) )
251 simplrr 760 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
z  e.  ( R1
`  C ) )
252251, 248eleqtrd 2514 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
z  e.  ~P ( R1 `  U. C ) )
253252elpwid 3865 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
z  C_  ( R1 ` 
U. C ) )
254 f1imaeq 5973 . . . . . . 7  |-  ( ( 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 ) )
255242, 250, 253, 254syl12anc 1216 . . . . . 6  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( ( H "
y )  =  ( H " z )  <-> 
y  =  z ) )
256231, 241, 2553bitrd 279 . . . . 5  |-  ( ( ( 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 ) )
257227, 256pm2.61dan 789 . . . 4  |-  ( (
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 ) )
258257ex 434 . . 3  |-  ( 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 ) ) )
259162, 258dom2lem 7341 . 2  |-  ( 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 )
260138, 76, 1, 5, 120dfac12lem1 8304 . . 3  |-  ( 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 ) ) ) ) )
261 f1eq1 5596 . . 3  |-  ( ( 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 ) )
262260, 261syl 16 . 2  |-  ( 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 ) )
263259, 262mpbird 232 1  |-  ( ph  ->  ( G `  C
) : ( R1
`  C ) -1-1-> On )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1369    e. wcel 1756    =/= wne 2601   A.wral 2710   _Vcvv 2967    C_ wss 3323   (/)c0 3632   ifcif 3786   ~Pcpw 3855   U.cuni 4086   class class class wbr 4287    e. cmpt 4345    _E cep 4625    We wwe 4673   Ord word 4713   Oncon0 4714   suc csuc 4716    X. cxp 4833   `'ccnv 4834   dom cdm 4835   ran crn 4836   "cima 4838    o. ccom 4839   Fun wfun 5407    Fn wfn 5408   -->wf 5409   -1-1->wf1 5410   -1-1-onto->wf1o 5412   ` cfv 5413    Isom wiso 5414  (class class class)co 6086  recscrecs 6823    +o coa 6909    .o comu 6910    ~~ cen 7299    ~<_ cdom 7300  OrdIsocoi 7715  harchar 7763   R1cr1 7961   rankcrnk 7962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-rep 4398  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-int 4124  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-se 4675  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-recs 6824  df-rdg 6858  df-oadd 6916  df-omul 6917  df-er 7093  df-en 7303  df-dom 7304  df-oi 7716  df-har 7765  df-r1 7963  df-rank 7964
This theorem is referenced by:  dfac12lem3  8306
  Copyright terms: Public domain W3C validator