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

Theorem dfac12lem2 8599
Description: Lemma for dfac12 8604. (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 7140 . . . . . . . . . . . . 13  |-  G  Fn  On
3 fnfun 5694 . . . . . . . . . . . . 13  |-  ( G  Fn  On  ->  Fun  G )
42, 3ax-mp 5 . . . . . . . . . . . 12  |-  Fun  G
5 dfac12.5 . . . . . . . . . . . 12  |-  ( ph  ->  C  e.  On )
6 funimaexg 5681 . . . . . . . . . . . 12  |-  ( ( Fun  G  /\  C  e.  On )  ->  ( G " C )  e. 
_V )
74, 5, 6sylancr 674 . . . . . . . . . . 11  |-  ( ph  ->  ( G " C
)  e.  _V )
8 uniexg 6614 . . . . . . . . . . 11  |-  ( ( G " C )  e.  _V  ->  U. ( G " C )  e. 
_V )
9 rnexg 6751 . . . . . . . . . . 11  |-  ( U. ( G " C )  e.  _V  ->  ran  U. ( G " C
)  e.  _V )
107, 8, 93syl 18 . . . . . . . . . 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 5801 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) : ( R1 `  z ) -1-1-> On  ->  ( G `  z ) : ( R1 `  z ) --> On )
13 fssxp 5763 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) : ( R1 `  z ) --> On  ->  ( G `  z ) 
C_  ( ( R1
`  z )  X.  On ) )
14 ssv 3463 . . . . . . . . . . . . . . . . . . . 20  |-  ( R1
`  z )  C_  _V
15 xpss1 4961 . . . . . . . . . . . . . . . . . . . 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 3451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( G `  z
)  C_  ( ( R1 `  z )  X.  On )  /\  (
( R1 `  z
)  X.  On ) 
C_  ( _V  X.  On ) )  ->  ( G `  z )  C_  ( _V  X.  On ) )
1816, 17mpan2 682 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  z ) 
C_  ( ( R1
`  z )  X.  On )  ->  ( G `  z )  C_  ( _V  X.  On ) )
19 fvex 5897 . . . . . . . . . . . . . . . . . . 19  |-  ( G `
 z )  e. 
_V
2019elpw 3968 . . . . . . . . . . . . . . . . . 18  |-  ( ( G `  z )  e.  ~P ( _V 
X.  On )  <->  ( G `  z )  C_  ( _V  X.  On ) )
2118, 20sylibr 217 . . . . . . . . . . . . . . . . 17  |-  ( ( G `  z ) 
C_  ( ( R1
`  z )  X.  On )  ->  ( G `  z )  e.  ~P ( _V  X.  On ) )
2212, 13, 213syl 18 . . . . . . . . . . . . . . . 16  |-  ( ( G `  z ) : ( R1 `  z ) -1-1-> On  ->  ( G `  z )  e.  ~P ( _V 
X.  On ) )
2322ralimi 2792 . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. z  e.  C  ( G `  z )  e.  ~P ( _V 
X.  On ) )
25 onss 6643 . . . . . . . . . . . . . . . . 17  |-  ( C  e.  On  ->  C  C_  On )
265, 25syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  C  C_  On )
27 fndm 5696 . . . . . . . . . . . . . . . . 17  |-  ( G  Fn  On  ->  dom  G  =  On )
282, 27ax-mp 5 . . . . . . . . . . . . . . . 16  |-  dom  G  =  On
2926, 28syl6sseqr 3490 . . . . . . . . . . . . . . 15  |-  ( ph  ->  C  C_  dom  G )
30 funimass4 5938 . . . . . . . . . . . . . . 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 674 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( G " C )  C_  ~P ( _V  X.  On ) 
<-> 
A. z  e.  C  ( G `  z )  e.  ~P ( _V 
X.  On ) ) )
3224, 31mpbird 240 . . . . . . . . . . . . 13  |-  ( ph  ->  ( G " C
)  C_  ~P ( _V  X.  On ) )
33 sspwuni 4380 . . . . . . . . . . . . 13  |-  ( ( G " C ) 
C_  ~P ( _V  X.  On )  <->  U. ( G " C )  C_  ( _V  X.  On ) )
3432, 33sylib 201 . . . . . . . . . . . 12  |-  ( ph  ->  U. ( G " C )  C_  ( _V  X.  On ) )
35 rnss 5081 . . . . . . . . . . . 12  |-  ( U. ( G " C ) 
C_  ( _V  X.  On )  ->  ran  U. ( G " C ) 
C_  ran  ( _V  X.  On ) )
3634, 35syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ran  U. ( G
" C )  C_  ran  ( _V  X.  On ) )
37 rnxpss 5287 . . . . . . . . . . 11  |-  ran  ( _V  X.  On )  C_  On
3836, 37syl6ss 3455 . . . . . . . . . 10  |-  ( ph  ->  ran  U. ( G
" C )  C_  On )
39 ssonuni 6639 . . . . . . . . . 10  |-  ( ran  U. ( G " C
)  e.  _V  ->  ( ran  U. ( G
" C )  C_  On  ->  U. ran  U. ( G " C )  e.  On ) )
4010, 38, 39sylc 62 . . . . . . . . 9  |-  ( ph  ->  U. ran  U. ( G " C )  e.  On )
41 suceloni 6666 . . . . . . . . 9  |-  ( U. ran  U. ( G " C )  e.  On  ->  suc  U. ran  U. ( G " C )  e.  On )
4240, 41syl 17 . . . . . . . 8  |-  ( ph  ->  suc  U. ran  U. ( G " C )  e.  On )
4342ad2antrr 737 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  suc  U. ran  U. ( G " C )  e.  On )
44 rankon 8291 . . . . . . 7  |-  ( rank `  y )  e.  On
45 omcl 7263 . . . . . . 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 673 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( suc  U. ran  U. ( G " C )  .o  ( rank `  y
) )  e.  On )
47 rankr1ai 8294 . . . . . . . . . . . 12  |-  ( y  e.  ( R1 `  C )  ->  ( rank `  y )  e.  C )
4847ad2antlr 738 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( rank `  y )  e.  C )
49 simpr 467 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  C  =  U. C )
5048, 49eleqtrd 2541 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( rank `  y )  e.  U. C )
51 eloni 5451 . . . . . . . . . . . . 13  |-  ( C  e.  On  ->  Ord  C )
525, 51syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  Ord  C )
5352ad2antrr 737 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  Ord  C )
54 ordsucuniel 6677 . . . . . . . . . . 11  |-  ( Ord 
C  ->  ( ( rank `  y )  e. 
U. C  <->  suc  ( rank `  y )  e.  C
) )
5553, 54syl 17 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( rank `  y
)  e.  U. C  <->  suc  ( rank `  y
)  e.  C ) )
5650, 55mpbid 215 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  suc  ( rank `  y
)  e.  C )
5711ad2antrr 737 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  A. z  e.  C  ( G `  z ) : ( R1 `  z ) -1-1-> On )
58 fveq2 5887 . . . . . . . . . . . 12  |-  ( z  =  suc  ( rank `  y )  ->  ( G `  z )  =  ( G `  suc  ( rank `  y
) ) )
59 f1eq1 5796 . . . . . . . . . . . 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 17 . . . . . . . . . . 11  |-  ( z  =  suc  ( rank `  y )  ->  (
( G `  z
) : ( R1
`  z ) -1-1-> On  <->  ( G `  suc  ( rank `  y ) ) : ( R1 `  z ) -1-1-> On ) )
61 fveq2 5887 . . . . . . . . . . . 12  |-  ( z  =  suc  ( rank `  y )  ->  ( R1 `  z )  =  ( R1 `  suc  ( rank `  y )
) )
62 f1eq2 5797 . . . . . . . . . . . 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 17 . . . . . . . . . . 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 261 . . . . . . . . . 10  |-  ( z  =  suc  ( rank `  y )  ->  (
( G `  z
) : ( R1
`  z ) -1-1-> On  <->  ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y
) ) -1-1-> On ) )
6564rspcv 3157 . . . . . . . . 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 62 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
) : ( R1
`  suc  ( rank `  y ) ) -1-1-> On )
67 f1f 5801 . . . . . . . 8  |-  ( ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y
) ) -1-1-> On  ->  ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y
) ) --> On )
6866, 67syl 17 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
) : ( R1
`  suc  ( rank `  y ) ) --> On )
69 r1elwf 8292 . . . . . . . . 9  |-  ( y  e.  ( R1 `  C )  ->  y  e.  U. ( R1 " On ) )
7069ad2antlr 738 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
y  e.  U. ( R1 " On ) )
71 rankidb 8296 . . . . . . . 8  |-  ( y  e.  U. ( R1
" On )  -> 
y  e.  ( R1
`  suc  ( rank `  y ) ) )
7270, 71syl 17 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
y  e.  ( R1
`  suc  ( rank `  y ) ) )
7368, 72ffvelrnd 6045 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  On )
74 oacl 7262 . . . . . 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 671 . . . . 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 5801 . . . . . . . 8  |-  ( F : ~P (har `  ( R1 `  A ) ) -1-1-> On  ->  F : ~P (har `  ( R1 `  A ) ) --> On )
7876, 77syl 17 . . . . . . 7  |-  ( ph  ->  F : ~P (har `  ( R1 `  A
) ) --> On )
7978ad2antrr 737 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  F : ~P (har `  ( R1 `  A ) ) --> On )
80 imassrn 5197 . . . . . . . 8  |-  ( H
" y )  C_  ran  H
81 fvex 5897 . . . . . . . . . . . . . . 15  |-  ( G `
 U. C )  e.  _V
8281rnex 6753 . . . . . . . . . . . . . 14  |-  ran  ( G `  U. C )  e.  _V
835ad2antrr 737 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  C  e.  On )
84 onuni 6646 . . . . . . . . . . . . . . . . . . 19  |-  ( C  e.  On  ->  U. C  e.  On )
85 sucidg 5519 . . . . . . . . . . . . . . . . . . 19  |-  ( U. C  e.  On  ->  U. C  e.  suc  U. C )
8683, 84, 853syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  U. C  e.  suc  U. C )
8752adantr 471 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  ( R1 `  C ) )  ->  Ord  C )
88 orduniorsuc 6683 . . . . . . . . . . . . . . . . . . . 20  |-  ( Ord 
C  ->  ( C  =  U. C  \/  C  =  suc  U. C ) )
8987, 88syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  ( R1 `  C ) )  ->  ( C  =  U. C  \/  C  =  suc  U. C ) )
9089orcanai 929 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  C  =  suc  U. C )
9186, 90eleqtrrd 2542 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  U. C  e.  C
)
9211ad2antrr 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  A. z  e.  C  ( G `  z ) : ( R1 `  z ) -1-1-> On )
93 fveq2 5887 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  U. C  -> 
( G `  z
)  =  ( G `
 U. C ) )
94 f1eq1 5796 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( G `  z )  =  ( G `  U. C )  ->  (
( G `  z
) : ( R1
`  z ) -1-1-> On  <->  ( G `  U. C
) : ( R1
`  z ) -1-1-> On ) )
9593, 94syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  U. C  -> 
( ( G `  z ) : ( R1 `  z )
-1-1-> On  <->  ( G `  U. C ) : ( R1 `  z )
-1-1-> On ) )
96 fveq2 5887 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  U. C  -> 
( R1 `  z
)  =  ( R1
`  U. C ) )
97 f1eq2 5797 . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  U. C  -> 
( ( G `  U. C ) : ( R1 `  z )
-1-1-> On  <->  ( G `  U. C ) : ( R1 `  U. C
) -1-1-> On ) )
9995, 98bitrd 261 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  U. C  -> 
( ( G `  z ) : ( R1 `  z )
-1-1-> On  <->  ( G `  U. C ) : ( R1 `  U. C
) -1-1-> On ) )
10099rspcv 3157 . . . . . . . . . . . . . . . . 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 62 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( G `  U. C ) : ( R1 `  U. C
) -1-1-> On )
102 f1f 5801 . . . . . . . . . . . . . . . 16  |-  ( ( G `  U. C
) : ( R1
`  U. C ) -1-1-> On  ->  ( G `  U. C ) : ( R1 `  U. C
) --> On )
103 frn 5757 . . . . . . . . . . . . . . . 16  |-  ( ( G `  U. C
) : ( R1
`  U. C ) --> On 
->  ran  ( G `  U. C )  C_  On )
104101, 102, 1033syl 18 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  ( G `  U. C )  C_  On )
105 epweon 6636 . . . . . . . . . . . . . . 15  |-  _E  We  On
106 wess 4839 . . . . . . . . . . . . . . 15  |-  ( ran  ( G `  U. C )  C_  On  ->  (  _E  We  On  ->  _E  We  ran  ( G `  U. C ) ) )
107104, 105, 106mpisyl 21 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  _E  We  ran  ( G `  U. C
) )
108 eqid 2461 . . . . . . . . . . . . . . 15  |- OrdIso (  _E  ,  ran  ( G `
 U. C ) )  = OrdIso (  _E  ,  ran  ( G `
 U. C ) )
109108oiiso 8077 . . . . . . . . . . . . . 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 674 . . . . . . . . . . . . 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 6240 . . . . . . . . . . . . 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 5848 . . . . . . . . . . . . 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 5835 . . . . . . . . . . . . 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 19 . . . . . . . . . . . 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 5847 . . . . . . . . . . . . 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 5835 . . . . . . . . . . . . 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 18 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( G `  U. C ) : ( R1 `  U. C
) -1-1-> ran  ( G `  U. C ) )
118 f1co 5810 . . . . . . . . . . . 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 671 . . . . . . . . . . 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 5796 . . . . . . . . . . . 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 217 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  H : ( R1 `  U. C
) -1-1-> dom OrdIso (  _E  ,  ran  ( G `  U. C ) ) )
124 f1f 5801 . . . . . . . . . 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 5757 . . . . . . . . . 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 18 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  H  C_  dom OrdIso (  _E  ,  ran  ( G `  U. C ) ) )
127 harcl 8101 . . . . . . . . . . 11  |-  (har `  ( R1 `  A ) )  e.  On
128127onordi 5545 . . . . . . . . . 10  |-  Ord  (har `  ( R1 `  A
) )
129108oion 8076 . . . . . . . . . . . 12  |-  ( ran  ( G `  U. C )  e.  _V  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  e.  On )
13082, 129mp1i 13 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  e.  On )
131108oien 8078 . . . . . . . . . . . . 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 674 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  ~~  ran  ( G `  U. C ) )
133 fvex 5897 . . . . . . . . . . . . . . 15  |-  ( R1
`  U. C )  e. 
_V
134133f1oen 7615 . . . . . . . . . . . . . 14  |-  ( ( G `  U. C
) : ( R1
`  U. C ) -1-1-onto-> ran  ( G `  U. C )  ->  ( R1 `  U. C )  ~~  ran  ( G `  U. C
) )
135 ensym 7643 . . . . . . . . . . . . . 14  |-  ( ( R1 `  U. C
)  ~~  ran  ( G `
 U. C )  ->  ran  ( G `  U. C )  ~~  ( R1 `  U. C
) )
136101, 115, 134, 1354syl 19 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  ( G `  U. C )  ~~  ( R1 `  U. C
) )
137 fvex 5897 . . . . . . . . . . . . . 14  |-  ( R1
`  A )  e. 
_V
138 dfac12.1 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  e.  On )
139138ad2antrr 737 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  A  e.  On )
140 dfac12.6 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  C  C_  A )
141140ad2antrr 737 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  C  C_  A
)
142141, 91sseldd 3444 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  U. C  e.  A
)
143 r1ord2 8277 . . . . . . . . . . . . . . 15  |-  ( A  e.  On  ->  ( U. C  e.  A  ->  ( R1 `  U. C )  C_  ( R1 `  A ) ) )
144139, 142, 143sylc 62 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  U. C )  C_  ( R1 `  A ) )
145 ssdomg 7640 . . . . . . . . . . . . . 14  |-  ( ( R1 `  A )  e.  _V  ->  (
( R1 `  U. C )  C_  ( R1 `  A )  -> 
( R1 `  U. C )  ~<_  ( R1
`  A ) ) )
146137, 144, 145mpsyl 65 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  U. C )  ~<_  ( R1
`  A ) )
147 endomtr 7652 . . . . . . . . . . . . 13  |-  ( ( ran  ( G `  U. C )  ~~  ( R1 `  U. C )  /\  ( R1 `  U. C )  ~<_  ( R1
`  A ) )  ->  ran  ( G `  U. C )  ~<_  ( R1 `  A ) )
148136, 146, 147syl2anc 671 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  ( G `  U. C )  ~<_  ( R1 `  A ) )
149 endomtr 7652 . . . . . . . . . . . 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 671 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  ~<_  ( R1 `  A ) )
151 elharval 8103 . . . . . . . . . . 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 675 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  e.  (har `  ( R1 `  A ) ) )
153 ordelss 5457 . . . . . . . . . 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 674 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  dom OrdIso (  _E  ,  ran  ( G `  U. C ) )  C_  (har `  ( R1 `  A ) ) )
155126, 154sstrd 3453 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ran  H  C_  (har `  ( R1 `  A
) ) )
15680, 155syl5ss 3454 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( H "
y )  C_  (har `  ( R1 `  A
) ) )
157 fvex 5897 . . . . . . . 8  |-  (har `  ( R1 `  A ) )  e.  _V
158157elpw2 4580 . . . . . . 7  |-  ( ( H " y )  e.  ~P (har `  ( R1 `  A ) )  <->  ( H "
y )  C_  (har `  ( R1 `  A
) ) )
159156, 158sylibr 217 . . . . . 6  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( H "
y )  e.  ~P (har `  ( R1 `  A ) ) )
16079, 159ffvelrnd 6045 . . . . 5  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( F `  ( H " y ) )  e.  On )
16175, 160ifclda 3924 . . . 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 440 . . 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 3898 . . . . . . . 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 3898 . . . . . . . 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 472 . . . . . 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 737 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  suc  U.
ran  U. ( G " C )  e.  On )
168 nsuceq0 5521 . . . . . . . 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 6681 . . . . . . . . . . 11  |-  ( ran  U. ( G " C
)  C_  On  ->  ran  U. ( G " C
)  C_  suc  U. ran  U. ( G " C
) )
17238, 171syl 17 . . . . . . . . . 10  |-  ( ph  ->  ran  U. ( G
" C )  C_  suc  U. ran  U. ( G " C ) )
173172ad2antrr 737 . . . . . . . . 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 737 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  C  C_  On )
176 fnfvima 6167 . . . . . . . . . . . 12  |-  ( ( G  Fn  On  /\  C  C_  On  /\  suc  ( rank `  y )  e.  C )  ->  ( G `  suc  ( rank `  y ) )  e.  ( G " C
) )
177174, 175, 56, 176syl3anc 1276 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
)  e.  ( G
" C ) )
178 elssuni 4240 . . . . . . . . . . 11  |-  ( ( G `  suc  ( rank `  y ) )  e.  ( G " C )  ->  ( G `  suc  ( rank `  y ) )  C_  U. ( G " C
) )
179 rnss 5081 . . . . . . . . . . 11  |-  ( ( G `  suc  ( rank `  y ) ) 
C_  U. ( G " C )  ->  ran  ( G `  suc  ( rank `  y ) ) 
C_  ran  U. ( G " C ) )
180177, 178, 1793syl 18 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  ->  ran  ( G `  suc  ( rank `  y )
)  C_  ran  U. ( G " C ) )
181 f1fn 5802 . . . . . . . . . . . 12  |-  ( ( G `  suc  ( rank `  y ) ) : ( R1 `  suc  ( rank `  y
) ) -1-1-> On  ->  ( G `  suc  ( rank `  y ) )  Fn  ( R1 `  suc  ( rank `  y
) ) )
18266, 181syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( G `  suc  ( rank `  y )
)  Fn  ( R1
`  suc  ( rank `  y ) ) )
183 fnfvelrn 6041 . . . . . . . . . . 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 671 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  ran  ( G `  suc  ( rank `  y ) ) )
185180, 184sseldd 3444 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  ran  U. ( G " C ) )
186173, 185sseldd 3444 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  y
) ) `  y
)  e.  suc  U. ran  U. ( G " C ) )
187186adantlrr 732 . . . . . . 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 8291 . . . . . . . 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 2527 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y  e.  ( R1
`  C )  <->  z  e.  ( R1 `  C ) ) )
191190anbi2d 715 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( ph  /\  y  e.  ( R1 `  C
) )  <->  ( ph  /\  z  e.  ( R1
`  C ) ) ) )
192191anbi1d 716 . . . . . . . . . 10  |-  ( y  =  z  ->  (
( ( ph  /\  y  e.  ( R1 `  C ) )  /\  C  =  U. C )  <-> 
( ( ph  /\  z  e.  ( R1 `  C ) )  /\  C  =  U. C ) ) )
193 fveq2 5887 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  ( rank `  y )  =  ( rank `  z
) )
194 suceq 5506 . . . . . . . . . . . . . 14  |-  ( (
rank `  y )  =  ( rank `  z
)  ->  suc  ( rank `  y )  =  suc  ( rank `  z )
)
195193, 194syl 17 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  suc  ( rank `  y )  =  suc  ( rank `  z
) )
196195fveq2d 5891 . . . . . . . . . . . 12  |-  ( y  =  z  ->  ( G `  suc  ( rank `  y ) )  =  ( G `  suc  ( rank `  z )
) )
197 id 22 . . . . . . . . . . . 12  |-  ( y  =  z  ->  y  =  z )
198196, 197fveq12d 5893 . . . . . . . . . . 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 326 . . . . . . . . 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 2117 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ( R1 `  C
) )  /\  C  =  U. C )  -> 
( ( G `  suc  ( rank `  z
) ) `  z
)  e.  suc  U. ran  U. ( G " C ) )
202201adantlrl 731 . . . . . . 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 7310 . . . . . . 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 1292 . . . . . 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 472 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  suc  ( rank `  y )  =  suc  ( rank `  z
) )
206205fveq2d 5891 . . . . . . . . . . . 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 5889 . . . . . . . . . . 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 2471 . . . . . . . . . 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 732 . . . . . . . . . . . 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 471 . . . . . . . . . . 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 732 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  ->  y  e.  ( R1 `  suc  ( rank `  y )
) )
212211adantr 471 . . . . . . . . . . 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 8292 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( R1 `  C )  ->  z  e.  U. ( R1 " On ) )
214 rankidb 8296 . . . . . . . . . . . . . . 15  |-  ( z  e.  U. ( R1
" On )  -> 
z  e.  ( R1
`  suc  ( rank `  z ) ) )
215213, 214syl 17 . . . . . . . . . . . . . 14  |-  ( z  e.  ( R1 `  C )  ->  z  e.  ( R1 `  suc  ( rank `  z )
) )
216215ad2antll 740 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( y  e.  ( R1 `  C
)  /\  z  e.  ( R1 `  C ) ) )  ->  z  e.  ( R1 `  suc  ( rank `  z )
) )
217216ad2antrr 737 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( y  e.  ( R1 `  C )  /\  z  e.  ( R1 `  C ) ) )  /\  C  =  U. C )  /\  ( rank `  y )  =  ( rank `  z
) )  ->  z  e.  ( R1 `  suc  ( rank `  z )
) )
218205fveq2d 5891 . . . . . . . . . . . 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 2542 . . . . . . . . . . 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 6187 . . . . . . . . . . 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 1274 . . . . . . . . . 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 263 . . . . . . . . 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 212 . . . . . . . 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 612 . . . . . . 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 539 . . . . . . 7  |-  ( y  =  z  ->  (
( rank `  y )  =  ( rank `  z
)  /\  ( ( G `  suc  ( rank `  y ) ) `  y )  =  ( ( G `  suc  ( rank `  z )
) `  z )
) )
226224, 225impbid1 208 . . . . . 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 287 . . . . 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 3901 . . . . . . . 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 3901 . . . . . . . 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 472 . . . . . 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 737 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  ->  F : ~P (har `  ( R1 `  A ) ) -1-1-> On )
233159adantlrr 732 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( H " y
)  e.  ~P (har `  ( R1 `  A
) ) )
234191anbi1d 716 . . . . . . . . . 10  |-  ( y  =  z  ->  (
( ( ph  /\  y  e.  ( R1 `  C ) )  /\  -.  C  =  U. C )  <->  ( ( ph  /\  z  e.  ( R1 `  C ) )  /\  -.  C  =  U. C ) ) )
235 imaeq2 5182 . . . . . . . . . . 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 326 . . . . . . . . 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 2117 . . . . . . . 8  |-  ( ( ( ph  /\  z  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( H "
z )  e.  ~P (har `  ( R1 `  A ) ) )
239238adantlrl 731 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( H " z
)  e.  ~P (har `  ( R1 `  A
) ) )
240 f1fveq 6187 . . . . . . 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 1274 . . . . . 6  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( ( F `  ( H " y ) )  =  ( F `
 ( H "
z ) )  <->  ( H " y )  =  ( H " z ) ) )
242123adantlrr 732 . . . . . . 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 775 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
y  e.  ( R1
`  C ) )
24490fveq2d 5891 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( R1 `  C
) )  /\  -.  C  =  U. C )  ->  ( R1 `  C )  =  ( R1 `  suc  U. C ) )
245 r1suc 8266 . . . . . . . . . . . 12  |-  ( U. C  e.  On  ->  ( R1 `  suc  U. C )  =  ~P ( R1 `  U. C
) )
24683, 84, 2453syl 18 . . . . . . . . . . 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 732 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( R1 `  C
)  =  ~P ( R1 `  U. C ) )
249243, 248eleqtrd 2541 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
y  e.  ~P ( R1 `  U. C ) )
250249elpwid 3972 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
y  C_  ( R1 ` 
U. C ) )
251 simplrr 776 . . . . . . . . 9  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
z  e.  ( R1
`  C ) )
252251, 248eleqtrd 2541 . . . . . . . 8  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
z  e.  ~P ( R1 `  U. C ) )
253252elpwid 3972 . . . . . . 7  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
z  C_  ( R1 ` 
U. C ) )
254 f1imaeq 6190 . . . . . . 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 1274 . . . . . 6  |-  ( ( ( ph  /\  (
y  e.  ( R1
`  C )  /\  z  e.  ( R1 `  C ) ) )  /\  -.  C  = 
U. C )  -> 
( ( H "
y )  =  ( H " z )  <-> 
y  =  z ) )
256231, 241, 2553bitrd 287 . . . . 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 805 . . . 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 440 . . 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 7634 . 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 8598 . . 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 5796 . . 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 17 . 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 240 1  |-  ( ph  ->  ( G `  C
) : ( R1
`  C ) -1-1-> On )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    = wceq 1454    e. wcel 1897    =/= wne 2632   A.wral 2748   _Vcvv 3056    C_ wss 3415   (/)c0 3742   ifcif 3892   ~Pcpw 3962   U.cuni 4211   class class class wbr 4415    |-> cmpt 4474    _E cep 4761    We wwe 4810    X. cxp 4850   `'ccnv 4851   dom cdm 4852   ran crn 4853   "cima 4855    o. ccom 4856   Ord word 5440   Oncon0 5441   suc csuc 5443   Fun wfun 5594    Fn wfn 5595   -->wf 5596   -1-1->wf1 5597   -1-1-onto->wf1o 5599   ` cfv 5600    Isom wiso 5601  (class class class)co 6314  recscrecs 7114    +o coa 7204    .o comu 7205    ~~ cen 7591    ~<_ cdom 7592  OrdIsocoi 8049  harchar 8096   R1cr1 8258   rankcrnk 8259
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-rep 4528  ax-sep 4538  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6609
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-reu 2755  df-rmo 2756  df-rab 2757  df-v 3058  df-sbc 3279  df-csb 3375  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-pss 3431  df-nul 3743  df-if 3893  df-pw 3964  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-int 4248  df-iun 4293  df-br 4416  df-opab 4475  df-mpt 4476  df-tr 4511  df-eprel 4763  df-id 4767  df-po 4773  df-so 4774  df-fr 4811  df-se 4812  df-we 4813  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-pred 5398  df-ord 5444  df-on 5445  df-lim 5446  df-suc 5447  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-isom 5609  df-riota 6276  df-ov 6317  df-oprab 6318  df-mpt2 6319  df-om 6719  df-wrecs 7053  df-recs 7115  df-rdg 7153  df-oadd 7211  df-omul 7212  df-er 7388  df-en 7595  df-dom 7596  df-oi 8050  df-har 8098  df-r1 8260  df-rank 8261
This theorem is referenced by:  dfac12lem3  8600
  Copyright terms: Public domain W3C validator