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

Theorem dfac12lem2 8515
Description: Lemma for dfac12 8520. (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 7058 . . . . . . . . . . . . 13  |-  G  Fn  On
3 fnfun 5660 . . . . . . . . . . . . 13  |-  ( G  Fn  On  ->  Fun  G )
42, 3ax-mp 5 . . . . . . . . . . . 12  |-  Fun  G
5 dfac12.5 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  On )
6 funimaexg 5647 . . . . . . . . . . . 12  |-  ( ( Fun  G  /\  C  e.  On )  ->  ( G " C )  e. 
_V )
74, 5, 6sylancr 661 . . . . . . . . . . 11  |-  ( ph  ->  ( G " C
)  e.  _V )
8 uniexg 6570 . . . . . . . . . . 11  |-  ( ( G " C )  e.  _V  ->  U. ( G " C )  e. 
_V )
9 rnexg 6705 . . . . . . . . . . 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 5763 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) : ( R1 `  z ) -1-1-> On  ->  ( G `  z ) : ( R1 `  z ) --> On )
13 fssxp 5725 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) : ( R1 `  z ) --> On  ->  ( G `  z ) 
C_  ( ( R1
`  z )  X.  On ) )
14 ssv 3509 . . . . . . . . . . . . . . . . . . . 20  |-  ( R1
`  z )  C_  _V
15 xpss1 5099 . . . . . . . . . . . . . . . . . . . 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 3497 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( G `  z
)  C_  ( ( R1 `  z )  X.  On )  /\  (
( R1 `  z
)  X.  On ) 
C_  ( _V  X.  On ) )  ->  ( G `  z )  C_  ( _V  X.  On ) )
1816, 17mpan2 669 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  z ) 
C_  ( ( R1
`  z )  X.  On )  ->  ( G `  z )  C_  ( _V  X.  On ) )
19 fvex 5858 . . . . . . . . . . . . . . . . . . 19  |-  ( G `
 z )  e. 
_V
2019elpw 4005 . . . . . . . . . . . . . . . . . 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 2847 . . . . . . . . . . . . . . 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 6599 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  On  ->  C  C_  On )
265, 25syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  C_  On )
27 fndm 5662 . . . . . . . . . . . . . . . . 17  |-  ( G  Fn  On  ->  dom  G  =  On )
282, 27ax-mp 5 . . . . . . . . . . . . . . . 16  |-  dom  G  =  On
2926, 28syl6sseqr 3536 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  C_  dom  G )
30 funimass4 5899 . . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . . 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 4404 . . . . . . . . . . . . 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 5220 . . . . . . . . . . . 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 5424 . . . . . . . . . . 11  |-  ran  ( _V  X.  On )  C_  On
3836, 37syl6ss 3501 . . . . . . . . . 10  |-  ( ph  ->  ran  U. ( G
" C )  C_  On )
39 ssonuni 6595 . . . . . . . . . 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 6621 . . . . . . . . 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 723 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  suc  U. ran  U. ( G " C )  e.  On )
44 rankon 8204 . . . . . . 7  |-  ( rank `  y )  e.  On
45 omcl 7178 . . . . . . 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 660 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( suc  U. ran  U. ( G " C )  .o  ( rank `  y
) )  e.  On )
47 rankr1ai 8207 . . . . . . . . . . . 12  |-  ( y  e.  ( R1 `  C )  ->  ( rank `  y )  e.  C )
4847ad2antlr 724 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( rank `  y )  e.  C )
49 simpr 459 . . . . . . . . . . 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 4877 . . . . . . . . . . . . 13  |-  ( C  e.  On  ->  Ord  C )
525, 51syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  C )
5352ad2antrr 723 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  Ord  C )
54 ordsucuniel 6632 . . . . . . . . . . 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 723 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  A. z  e.  C  ( G `  z ) : ( R1 `  z ) -1-1-> On )
58 fveq2 5848 . . . . . . . . . . . 12  |-  ( z  =  suc  ( rank `  y )  ->  ( G `  z )  =  ( G `  suc  ( rank `  y
) ) )
59 f1eq1 5758 . . . . . . . . . . . 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 5848 . . . . . . . . . . . 12  |-  ( z  =  suc  ( rank `  y )  ->  ( R1 `  z )  =  ( R1 `  suc  ( rank `  y )
) )
62 f1eq2 5759 . . . . . . . . . . . 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 3203 . . . . . . . . 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 5763 . . . . . . . 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 8205 . . . . . . . . 9  |-  ( y  e.  ( R1 `  C )  ->  y  e.  U. ( R1 " On ) )
7069ad2antlr 724 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
y  e.  U. ( R1 " On ) )
71 rankidb 8209 . . . . . . . 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 6008 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  On )
74 oacl 7177 . . . . . 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 659 . . . . 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 5763 . . . . . . . 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 723 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  F : ~P (har `  ( R1 `  A ) ) --> On )
80 imassrn 5336 . . . . . . . 8  |-  ( H
" y )  C_  ran  H
81 fvex 5858 . . . . . . . . . . . . . . 15  |-  ( G `
 U. C )  e.  _V
8281rnex 6707 . . . . . . . . . . . . . 14  |-  ran  ( G `  U. C )  e.  _V
835ad2antrr 723 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  C  e.  On )
84 onuni 6601 . . . . . . . . . . . . . . . . . . 19  |-  ( C  e.  On  ->  U. C  e.  On )
85 sucidg 4945 . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  ( R1 `  C ) )  ->  Ord  C )
88 orduniorsuc 6638 . . . . . . . . . . . . . . . . . . . 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 911 . . . . . . . . . . . . . . . . . 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 723 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  A. z  e.  C  ( G `  z ) : ( R1 `  z ) -1-1-> On )
93 fveq2 5848 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  U. C  -> 
( G `  z
)  =  ( G `
 U. C ) )
94 f1eq1 5758 . . . . . . . . . . . . . . . . . . . 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 5848 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  U. C  -> 
( R1 `  z
)  =  ( R1
`  U. C ) )
97 f1eq2 5759 . . . . . . . . . . . . . . . . . . . 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 3203 . . . . . . . . . . . . . . . . 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 5763 . . . . . . . . . . . . . . . 16  |-  ( ( G `  U. C
) : ( R1
`  U. C ) -1-1-> On  ->  ( G `  U. C ) : ( R1 `  U. C
) --> On )
103 frn 5719 . . . . . . . . . . . . . . . 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 6592 . . . . . . . . . . . . . . 15  |-  _E  We  On
106 wess 4855 . . . . . . . . . . . . . . 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 7954 . . . . . . . . . . . . . 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 661 . . . . . . . . . . . . 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 6196 . . . . . . . . . . . . 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 5810 . . . . . . . . . . . . 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 5797 . . . . . . . . . . . . 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 5809 . . . . . . . . . . . . 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 5797 . . . . . . . . . . . . 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 5772 . . . . . . . . . . . 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 659 . . . . . . . . . . 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 5758 . . . . . . . . . . . 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 5763 . . . . . . . . . 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 5719 . . . . . . . . . 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 7979 . . . . . . . . . . 11  |-  (har `  ( R1 `  A ) )  e.  On
128127onordi 4971 . . . . . . . . . 10  |-  Ord  (har `  ( R1 `  A
) )
129108oion 7953 . . . . . . . . . . . 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 7955 . . . . . . . . . . . . 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 661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  ~~  ran  ( G `  U. C ) )
133 fvex 5858 . . . . . . . . . . . . . . 15  |-  ( R1
`  U. C )  e. 
_V
134133f1oen 7529 . . . . . . . . . . . . . 14  |-  ( ( G `  U. C
) : ( R1
`  U. C ) -1-1-onto-> ran  ( G `  U. C )  ->  ( R1 `  U. C )  ~~  ran  ( G `  U. C
) )
135 ensym 7557 . . . . . . . . . . . . . 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 5858 . . . . . . . . . . . . . 14  |-  ( R1
`  A )  e. 
_V
138 dfac12.1 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  On )
139138ad2antrr 723 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  A  e.  On )
140 dfac12.6 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  C  C_  A )
141140ad2antrr 723 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  C  C_  A
)
142141, 91sseldd 3490 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  U. C  e.  A
)
143 r1ord2 8190 . . . . . . . . . . . . . . 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 7554 . . . . . . . . . . . . . 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 7566 . . . . . . . . . . . . 13  |-  ( ( ran  ( G `  U. C )  ~~  ( R1 `  U. C )  /\  ( R1 `  U. C )  ~<_  ( R1
`  A ) )  ->  ran  ( G `  U. C )  ~<_  ( R1 `  A ) )
148136, 146, 147syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  ( G `  U. C )  ~<_  ( R1 `  A ) )
149 endomtr 7566 . . . . . . . . . . . 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 659 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  ~<_  ( R1 `  A ) )
151 elharval 7981 . . . . . . . . . . 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 662 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  e.  (har `  ( R1 `  A ) ) )
153 ordelss 4883 . . . . . . . . . 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 661 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  C_  (har `  ( R1 `  A ) ) )
155126, 154sstrd 3499 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  H  C_  (har `  ( R1 `  A
) ) )
15680, 155syl5ss 3500 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( H "
y )  C_  (har `  ( R1 `  A
) ) )
157 fvex 5858 . . . . . . . 8  |-  (har `  ( R1 `  A ) )  e.  _V
158157elpw2 4601 . . . . . . 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 6008 . . . . 5  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( F `  ( H " y ) )  e.  On )
16175, 160ifclda 3961 . . . 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 432 . . 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 3935 . . . . . . . 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 3935 . . . . . . . 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 464 . . . . . 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 723 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  suc  U.
ran  U. ( G " C )  e.  On )
168 nsuceq0 4947 . . . . . . . 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 6636 . . . . . . . . . . 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 723 . . . . . . . . 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 723 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  C  C_  On )
176 fnfvima 6125 . . . . . . . . . . . 12  |-  ( ( G  Fn  On  /\  C  C_  On  /\  suc  ( rank `  y )  e.  C )  ->  ( G `  suc  ( rank `  y ) )  e.  ( G " C
) )
177174, 175, 56, 176syl3anc 1226 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
)  e.  ( G
" C ) )
178 elssuni 4264 . . . . . . . . . . 11  |-  ( ( G `  suc  ( rank `  y ) )  e.  ( G " C )  ->  ( G `  suc  ( rank `  y ) )  C_  U. ( G " C
) )
179 rnss 5220 . . . . . . . . . . 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 5764 . . . . . . . . . . . 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 6004 . . . . . . . . . . 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 659 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  ran  ( G `  suc  ( rank `  y ) ) )
185180, 184sseldd 3490 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  ran  U. ( G " C ) )
186173, 185sseldd 3490 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  suc  U. ran  U. ( G " C ) )
187186adantlrr 718 . . . . . . 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 8204 . . . . . . . 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 701 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( ph  /\  y  e.  ( R1 `  C
) )  <->  ( ph  /\  z  e.  ( R1
`  C ) ) ) )
192191anbi1d 702 . . . . . . . . . 10  |-  ( y  =  z  ->  (
( ( ph  /\  y  e.  ( R1 `  C ) )  /\  C  =  U. C )  <-> 
( ( ph  /\  z  e.  ( R1 `  C ) )  /\  C  =  U. C ) ) )
193 fveq2 5848 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  ( rank `  y )  =  ( rank `  z
) )
194 suceq 4932 . . . . . . . . . . . . . 14  |-  ( (
rank `  y )  =  ( rank `  z
)  ->  suc  ( rank `  y )  =  suc  ( rank `  z )
)
195193, 194syl 16 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  suc  ( rank `  y )  =  suc  ( rank `  z
) )
196195fveq2d 5852 . . . . . . . . . . . 12  |-  ( y  =  z  ->  ( G `  suc  ( rank `  y ) )  =  ( G `  suc  ( rank `  z )
) )
197 id 22 . . . . . . . . . . . 12  |-  ( y  =  z  ->  y  =  z )
198196, 197fveq12d 5854 . . . . . . . . . . 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 318 . . . . . . . . 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 2019 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  z
) ) `  z
)  e.  suc  U. ran  U. ( G " C ) )
202201adantlrl 717 . . . . . . 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 7225 . . . . . . 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 1242 . . . . . 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 464 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  suc  ( rank `  y )  =  suc  ( rank `  z
) )
206205fveq2d 5852 . . . . . . . . . . . 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 5850 . . . . . . . . . . 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 718 . . . . . . . . . . . 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 463 . . . . . . . . . . 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 718 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  y  e.  ( R1 `  suc  ( rank `  y )
) )
212211adantr 463 . . . . . . . . . . 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 8205 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( R1 `  C )  ->  z  e.  U. ( R1 " On ) )
214 rankidb 8209 . . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  ( R1 `  C
)  /\  z  e.  ( R1 `  C ) ) )  ->  z  e.  ( R1 `  suc  ( rank `  z )
) )
217216ad2antrr 723 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  z  e.  ( R1 `  suc  ( rank `  z )
) )
218205fveq2d 5852 . . . . . . . . . . . 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 6145 . . . . . . . . . . 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 1224 . . . . . . . . . 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 601 . . . . . . 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 530 . . . . . . 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 3938 . . . . . . . 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 3938 . . . . . . . 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 464 . . . . . 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 723 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  ->  F : ~P (har `  ( R1 `  A ) ) -1-1-> On )
233159adantlrr 718 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( H " y
)  e.  ~P (har `  ( R1 `  A
) ) )
234191anbi1d 702 . . . . . . . . . 10  |-  ( y  =  z  ->  (
( ( ph  /\  y  e.  ( R1 `  C ) )  /\  -.  C  =  U. C )  <->  ( ( ph  /\  z  e.  ( R1 `  C ) )  /\  -.  C  =  U. C ) ) )
235 imaeq2 5321 . . . . . . . . . . 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 318 . . . . . . . . 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 2019 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( H "
z )  e.  ~P (har `  ( R1 `  A ) ) )
239238adantlrl 717 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( H " z
)  e.  ~P (har `  ( R1 `  A
) ) )
240 f1fveq 6145 . . . . . . 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 1224 . . . . . 6  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( ( F `  ( H " y ) )  =  ( F `
 ( H "
z ) )  <->  ( H " y )  =  ( H " z ) ) )
242123adantlrr 718 . . . . . . 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 5852 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  C )  =  ( R1 `  suc  U. C ) )
245 r1suc 8179 . . . . . . . . . . . 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 718 . . . . . . . . 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 4009 . . . . . . 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 4009 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
z  C_  ( R1 ` 
U. C ) )
254 f1imaeq 6148 . . . . . . 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 1224 . . . . . 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 432 . . 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 7548 . 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 8514 . . 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 5758 . . 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 366    /\ wa 367    = wceq 1398    e. wcel 1823    =/= wne 2649   A.wral 2804   _Vcvv 3106    C_ wss 3461   (/)c0 3783   ifcif 3929   ~Pcpw 3999   U.cuni 4235   class class class wbr 4439    |-> cmpt 4497    _E cep 4778    We wwe 4826   Ord word 4866   Oncon0 4867   suc csuc 4869    X. cxp 4986   `'ccnv 4987   dom cdm 4988   ran crn 4989   "cima 4991    o. ccom 4992   Fun wfun 5564    Fn wfn 5565   -->wf 5566   -1-1->wf1 5567   -1-1-onto->wf1o 5569   ` cfv 5570    Isom wiso 5571  (class class class)co 6270  recscrecs 7033    +o coa 7119    .o comu 7120    ~~ cen 7506    ~<_ cdom 7507  OrdIsocoi 7926  harchar 7974   R1cr1 8171   rankcrnk 8172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-se 4828  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-isom 5579  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-recs 7034  df-rdg 7068  df-oadd 7126  df-omul 7127  df-er 7303  df-en 7510  df-dom 7511  df-oi 7927  df-har 7976  df-r1 8173  df-rank 8174
This theorem is referenced by:  dfac12lem3  8516
  Copyright terms: Public domain W3C validator