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

Theorem dfac12lem2 8427
Description: Lemma for dfac12 8432. (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 6969 . . . . . . . . . . . . 13  |-  G  Fn  On
3 fnfun 5619 . . . . . . . . . . . . 13  |-  ( G  Fn  On  ->  Fun  G )
42, 3ax-mp 5 . . . . . . . . . . . 12  |-  Fun  G
5 dfac12.5 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  On )
6 funimaexg 5606 . . . . . . . . . . . 12  |-  ( ( Fun  G  /\  C  e.  On )  ->  ( G " C )  e. 
_V )
74, 5, 6sylancr 663 . . . . . . . . . . 11  |-  ( ph  ->  ( G " C
)  e.  _V )
8 uniexg 6490 . . . . . . . . . . 11  |-  ( ( G " C )  e.  _V  ->  U. ( G " C )  e. 
_V )
9 rnexg 6623 . . . . . . . . . . 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 5717 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) : ( R1 `  z ) -1-1-> On  ->  ( G `  z ) : ( R1 `  z ) --> On )
13 fssxp 5681 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) : ( R1 `  z ) --> On  ->  ( G `  z ) 
C_  ( ( R1
`  z )  X.  On ) )
14 ssv 3487 . . . . . . . . . . . . . . . . . . . 20  |-  ( R1
`  z )  C_  _V
15 xpss1 5059 . . . . . . . . . . . . . . . . . . . 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 3475 . . . . . . . . . . . . . . . . . . 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 5812 . . . . . . . . . . . . . . . . . . 19  |-  ( G `
 z )  e. 
_V
2019elpw 3977 . . . . . . . . . . . . . . . . . 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 2819 . . . . . . . . . . . . . . 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 6515 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  On  ->  C  C_  On )
265, 25syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  C_  On )
27 fndm 5621 . . . . . . . . . . . . . . . . 17  |-  ( G  Fn  On  ->  dom  G  =  On )
282, 27ax-mp 5 . . . . . . . . . . . . . . . 16  |-  dom  G  =  On
2926, 28syl6sseqr 3514 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  C_  dom  G )
30 funimass4 5854 . . . . . . . . . . . . . . 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 4367 . . . . . . . . . . . . 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 5179 . . . . . . . . . . . 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 5381 . . . . . . . . . . 11  |-  ran  ( _V  X.  On )  C_  On
3836, 37syl6ss 3479 . . . . . . . . . 10  |-  ( ph  ->  ran  U. ( G
" C )  C_  On )
39 ssonuni 6511 . . . . . . . . . 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 6537 . . . . . . . . 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 8116 . . . . . . 7  |-  ( rank `  y )  e.  On
45 omcl 7089 . . . . . . 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 8119 . . . . . . . . . . . 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 2544 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( rank `  y )  e.  U. C )
51 eloni 4840 . . . . . . . . . . . . 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 6548 . . . . . . . . . . 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 5802 . . . . . . . . . . . 12  |-  ( z  =  suc  ( rank `  y )  ->  ( G `  z )  =  ( G `  suc  ( rank `  y
) ) )
59 f1eq1 5712 . . . . . . . . . . . 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 5802 . . . . . . . . . . . 12  |-  ( z  =  suc  ( rank `  y )  ->  ( R1 `  z )  =  ( R1 `  suc  ( rank `  y )
) )
62 f1eq2 5713 . . . . . . . . . . . 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 3175 . . . . . . . . 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 5717 . . . . . . . 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 8117 . . . . . . . . 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 8121 . . . . . . . 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 5956 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  On )
74 oacl 7088 . . . . . 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 5717 . . . . . . . 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 5291 . . . . . . . 8  |-  ( H
" y )  C_  ran  H
81 fvex 5812 . . . . . . . . . . . . . . 15  |-  ( G `
 U. C )  e.  _V
8281rnex 6625 . . . . . . . . . . . . . 14  |-  ran  ( G `  U. C )  e.  _V
835ad2antrr 725 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  C  e.  On )
84 onuni 6517 . . . . . . . . . . . . . . . . . . 19  |-  ( C  e.  On  ->  U. C  e.  On )
85 sucidg 4908 . . . . . . . . . . . . . . . . . . 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 6554 . . . . . . . . . . . . . . . . . . . 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 2545 . . . . . . . . . . . . . . . . 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 5802 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  U. C  -> 
( G `  z
)  =  ( G `
 U. C ) )
94 f1eq1 5712 . . . . . . . . . . . . . . . . . . . 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 5802 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  U. C  -> 
( R1 `  z
)  =  ( R1
`  U. C ) )
97 f1eq2 5713 . . . . . . . . . . . . . . . . . . . 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 3175 . . . . . . . . . . . . . . . . 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 5717 . . . . . . . . . . . . . . . 16  |-  ( ( G `  U. C
) : ( R1
`  U. C ) -1-1-> On  ->  ( G `  U. C ) : ( R1 `  U. C
) --> On )
103 frn 5676 . . . . . . . . . . . . . . . 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 6508 . . . . . . . . . . . . . . 15  |-  _E  We  On
106 wess 4818 . . . . . . . . . . . . . . 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 2454 . . . . . . . . . . . . . . 15  |- OrdIso (  _E  ,  ran  ( G `
 U. C ) )  = OrdIso (  _E  ,  ran  ( G `
 U. C ) )
109108oiiso 7865 . . . . . . . . . . . . . 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 6128 . . . . . . . . . . . . 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 5764 . . . . . . . . . . . . 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 5751 . . . . . . . . . . . . 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 5763 . . . . . . . . . . . . 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 5751 . . . . . . . . . . . . 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 5726 . . . . . . . . . . . 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 5712 . . . . . . . . . . . 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 5717 . . . . . . . . . 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 5676 . . . . . . . . . 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 7890 . . . . . . . . . . 11  |-  (har `  ( R1 `  A ) )  e.  On
128127onordi 4934 . . . . . . . . . 10  |-  Ord  (har `  ( R1 `  A
) )
129108oion 7864 . . . . . . . . . . . 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 7866 . . . . . . . . . . . . 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 5812 . . . . . . . . . . . . . . 15  |-  ( R1
`  U. C )  e. 
_V
134133f1oen 7443 . . . . . . . . . . . . . 14  |-  ( ( G `  U. C
) : ( R1
`  U. C ) -1-1-onto-> ran  ( G `  U. C )  ->  ( R1 `  U. C )  ~~  ran  ( G `  U. C
) )
135 ensym 7471 . . . . . . . . . . . . . 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 5812 . . . . . . . . . . . . . 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 3468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  U. C  e.  A
)
143 r1ord2 8102 . . . . . . . . . . . . . . 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 7468 . . . . . . . . . . . . . 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 7480 . . . . . . . . . . . . 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 7480 . . . . . . . . . . . 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 7892 . . . . . . . . . . 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 4846 . . . . . . . . . 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 3477 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  H  C_  (har `  ( R1 `  A
) ) )
15680, 155syl5ss 3478 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( H "
y )  C_  (har `  ( R1 `  A
) ) )
157 fvex 5812 . . . . . . . 8  |-  (har `  ( R1 `  A ) )  e.  _V
158157elpw2 4567 . . . . . . 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 5956 . . . . 5  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( F `  ( H " y ) )  e.  On )
16175, 160ifclda 3932 . . . 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 3908 . . . . . . . 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 3908 . . . . . . . 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 2476 . . . . . . 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 4910 . . . . . . . 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 6552 . . . . . . . . . . 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 6067 . . . . . . . . . . . 12  |-  ( ( G  Fn  On  /\  C  C_  On  /\  suc  ( rank `  y )  e.  C )  ->  ( G `  suc  ( rank `  y ) )  e.  ( G " C
) )
177174, 175, 56, 176syl3anc 1219 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
)  e.  ( G
" C ) )
178 elssuni 4232 . . . . . . . . . . 11  |-  ( ( G `  suc  ( rank `  y ) )  e.  ( G " C )  ->  ( G `  suc  ( rank `  y ) )  C_  U. ( G " C
) )
179 rnss 5179 . . . . . . . . . . 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 5718 . . . . . . . . . . . 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 5952 . . . . . . . . . . 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 3468 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  ran  U. ( G " C ) )
186173, 185sseldd 3468 . . . . . . . 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 8116 . . . . . . . 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 2526 . . . . . . . . . . . 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 5802 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  ( rank `  y )  =  ( rank `  z
) )
194 suceq 4895 . . . . . . . . . . . . . 14  |-  ( (
rank `  y )  =  ( rank `  z
)  ->  suc  ( rank `  y )  =  suc  ( rank `  z )
)
195193, 194syl 16 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  suc  ( rank `  y )  =  suc  ( rank `  z
) )
196195fveq2d 5806 . . . . . . . . . . . 12  |-  ( y  =  z  ->  ( G `  suc  ( rank `  y ) )  =  ( G `  suc  ( rank `  z )
) )
197 id 22 . . . . . . . . . . . 12  |-  ( y  =  z  ->  y  =  z )
198196, 197fveq12d 5808 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( G `  suc  ( rank `  y )
) `  y )  =  ( ( G `
 suc  ( rank `  z ) ) `  z ) )
199198eleq1d 2523 . . . . . . . . . 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 1970 . . . . . . . 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 7136 . . . . . . 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 1235 . . . . . 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 5806 . . . . . . . . . . . 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 5804 . . . . . . . . . . 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 2468 . . . . . . . . . 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 8117 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( R1 `  C )  ->  z  e.  U. ( R1 " On ) )
214 rankidb 8121 . . . . . . . . . . . . . . 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 5806 . . . . . . . . . . . 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 2545 . . . . . . . . . . 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 6087 . . . . . . . . . . 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 1217 . . . . . . . . . 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 3910 . . . . . . . 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 3910 . . . . . . . 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 2476 . . . . . . 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 5276 . . . . . . . . . . 11  |-  ( y  =  z  ->  ( H " y )  =  ( H " z
) )
236235eleq1d 2523 . . . . . . . . . 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 1970 . . . . . . . 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 6087 . . . . . . 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 1217 . . . . . 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 5806 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  C )  =  ( R1 `  suc  U. C ) )
245 r1suc 8091 . . . . . . . . . . . 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 2495 . . . . . . . . . 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 2544 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
y  e.  ~P ( R1 `  U. C ) )
250249elpwid 3981 . . . . . . 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 2544 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
z  e.  ~P ( R1 `  U. C ) )
253252elpwid 3981 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
z  C_  ( R1 ` 
U. C ) )
254 f1imaeq 6090 . . . . . . 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 1217 . . . . . 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 7462 . 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 8426 . . 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 5712 . . 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 1370    e. wcel 1758    =/= wne 2648   A.wral 2799   _Vcvv 3078    C_ wss 3439   (/)c0 3748   ifcif 3902   ~Pcpw 3971   U.cuni 4202   class class class wbr 4403    |-> cmpt 4461    _E cep 4741    We wwe 4789   Ord word 4829   Oncon0 4830   suc csuc 4832    X. cxp 4949   `'ccnv 4950   dom cdm 4951   ran crn 4952   "cima 4954    o. ccom 4955   Fun wfun 5523    Fn wfn 5524   -->wf 5525   -1-1->wf1 5526   -1-1-onto->wf1o 5528   ` cfv 5529    Isom wiso 5530  (class class class)co 6203  recscrecs 6944    +o coa 7030    .o comu 7031    ~~ cen 7420    ~<_ cdom 7421  OrdIsocoi 7837  harchar 7885   R1cr1 8083   rankcrnk 8084
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-pss 3455  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-tp 3993  df-op 3995  df-uni 4203  df-int 4240  df-iun 4284  df-br 4404  df-opab 4462  df-mpt 4463  df-tr 4497  df-eprel 4743  df-id 4747  df-po 4752  df-so 4753  df-fr 4790  df-se 4791  df-we 4792  df-ord 4833  df-on 4834  df-lim 4835  df-suc 4836  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-isom 5538  df-riota 6164  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-om 6590  df-recs 6945  df-rdg 6979  df-oadd 7037  df-omul 7038  df-er 7214  df-en 7424  df-dom 7425  df-oi 7838  df-har 7887  df-r1 8085  df-rank 8086
This theorem is referenced by:  dfac12lem3  8428
  Copyright terms: Public domain W3C validator