ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ennnfonelemhf1o Unicode version

Theorem ennnfonelemhf1o 12427
Description: Lemma for ennnfone 12439. Each of the functions in  H is one to one and onto an image of  F. (Contributed by Jim Kingdon, 17-Jul-2023.)
Hypotheses
Ref Expression
ennnfonelemh.dceq  |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
ennnfonelemh.f  |-  ( ph  ->  F : om -onto-> A
)
ennnfonelemh.ne  |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
ennnfonelemh.g  |-  G  =  ( x  e.  ( A  ^pm  om ) ,  y  e.  om  |->  if ( ( F `  y )  e.  ( F " y ) ,  x ,  ( x  u.  { <. dom  x ,  ( F `
 y ) >. } ) ) )
ennnfonelemh.n  |-  N  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
ennnfonelemh.j  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
ennnfonelemh.h  |-  H  =  seq 0 ( G ,  J )
ennnfonelemhf1o.p  |-  ( ph  ->  P  e.  NN0 )
Assertion
Ref Expression
ennnfonelemhf1o  |-  ( ph  ->  ( H `  P
) : dom  ( H `  P ) -1-1-onto-> ( F " ( `' N `  P ) ) )
Distinct variable groups:    A, j, x, y    j, F, k, x, y    j, G   
j, H, k, x, y    j, J    j, N, k, x, y    ph, j,
k, x, y
Allowed substitution hints:    ph( n)    A( k, n)    P( x, y, j, k, n)    F( n)    G( x, y, k, n)    H( n)    J( x, y, k, n)    N( n)

Proof of Theorem ennnfonelemhf1o
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 ennnfonelemhf1o.p . 2  |-  ( ph  ->  P  e.  NN0 )
2 fveq2 5527 . . . . 5  |-  ( w  =  0  ->  ( H `  w )  =  ( H ` 
0 ) )
32dmeqd 4841 . . . . 5  |-  ( w  =  0  ->  dom  ( H `  w )  =  dom  ( H `
 0 ) )
4 fveq2 5527 . . . . . 6  |-  ( w  =  0  ->  ( `' N `  w )  =  ( `' N `  0 ) )
54imaeq2d 4982 . . . . 5  |-  ( w  =  0  ->  ( F " ( `' N `  w ) )  =  ( F " ( `' N `  0 ) ) )
62, 3, 5f1oeq123d 5467 . . . 4  |-  ( w  =  0  ->  (
( H `  w
) : dom  ( H `  w ) -1-1-onto-> ( F " ( `' N `  w ) )  <->  ( H `  0 ) : dom  ( H ` 
0 ) -1-1-onto-> ( F " ( `' N `  0 ) ) ) )
76imbi2d 230 . . 3  |-  ( w  =  0  ->  (
( ph  ->  ( H `
 w ) : dom  ( H `  w ) -1-1-onto-> ( F " ( `' N `  w ) ) )  <->  ( ph  ->  ( H `  0
) : dom  ( H `  0 ) -1-1-onto-> ( F " ( `' N `  0 ) ) ) ) )
8 fveq2 5527 . . . . 5  |-  ( w  =  k  ->  ( H `  w )  =  ( H `  k ) )
98dmeqd 4841 . . . . 5  |-  ( w  =  k  ->  dom  ( H `  w )  =  dom  ( H `
 k ) )
10 fveq2 5527 . . . . . 6  |-  ( w  =  k  ->  ( `' N `  w )  =  ( `' N `  k ) )
1110imaeq2d 4982 . . . . 5  |-  ( w  =  k  ->  ( F " ( `' N `  w ) )  =  ( F " ( `' N `  k ) ) )
128, 9, 11f1oeq123d 5467 . . . 4  |-  ( w  =  k  ->  (
( H `  w
) : dom  ( H `  w ) -1-1-onto-> ( F " ( `' N `  w ) )  <->  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) ) )
1312imbi2d 230 . . 3  |-  ( w  =  k  ->  (
( ph  ->  ( H `
 w ) : dom  ( H `  w ) -1-1-onto-> ( F " ( `' N `  w ) ) )  <->  ( ph  ->  ( H `  k
) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) ) ) )
14 fveq2 5527 . . . . 5  |-  ( w  =  ( k  +  1 )  ->  ( H `  w )  =  ( H `  ( k  +  1 ) ) )
1514dmeqd 4841 . . . . 5  |-  ( w  =  ( k  +  1 )  ->  dom  ( H `  w )  =  dom  ( H `
 ( k  +  1 ) ) )
16 fveq2 5527 . . . . . 6  |-  ( w  =  ( k  +  1 )  ->  ( `' N `  w )  =  ( `' N `  ( k  +  1 ) ) )
1716imaeq2d 4982 . . . . 5  |-  ( w  =  ( k  +  1 )  ->  ( F " ( `' N `  w ) )  =  ( F " ( `' N `  ( k  +  1 ) ) ) )
1814, 15, 17f1oeq123d 5467 . . . 4  |-  ( w  =  ( k  +  1 )  ->  (
( H `  w
) : dom  ( H `  w ) -1-1-onto-> ( F " ( `' N `  w ) )  <->  ( H `  ( k  +  1 ) ) : dom  ( H `  ( k  +  1 ) ) -1-1-onto-> ( F " ( `' N `  ( k  +  1 ) ) ) ) )
1918imbi2d 230 . . 3  |-  ( w  =  ( k  +  1 )  ->  (
( ph  ->  ( H `
 w ) : dom  ( H `  w ) -1-1-onto-> ( F " ( `' N `  w ) ) )  <->  ( ph  ->  ( H `  (
k  +  1 ) ) : dom  ( H `  ( k  +  1 ) ) -1-1-onto-> ( F " ( `' N `  ( k  +  1 ) ) ) ) ) )
20 fveq2 5527 . . . . 5  |-  ( w  =  P  ->  ( H `  w )  =  ( H `  P ) )
2120dmeqd 4841 . . . . 5  |-  ( w  =  P  ->  dom  ( H `  w )  =  dom  ( H `
 P ) )
22 fveq2 5527 . . . . . 6  |-  ( w  =  P  ->  ( `' N `  w )  =  ( `' N `  P ) )
2322imaeq2d 4982 . . . . 5  |-  ( w  =  P  ->  ( F " ( `' N `  w ) )  =  ( F " ( `' N `  P ) ) )
2420, 21, 23f1oeq123d 5467 . . . 4  |-  ( w  =  P  ->  (
( H `  w
) : dom  ( H `  w ) -1-1-onto-> ( F " ( `' N `  w ) )  <->  ( H `  P ) : dom  ( H `  P ) -1-1-onto-> ( F " ( `' N `  P ) ) ) )
2524imbi2d 230 . . 3  |-  ( w  =  P  ->  (
( ph  ->  ( H `
 w ) : dom  ( H `  w ) -1-1-onto-> ( F " ( `' N `  w ) ) )  <->  ( ph  ->  ( H `  P
) : dom  ( H `  P ) -1-1-onto-> ( F " ( `' N `  P ) ) ) ) )
26 f1o0 5510 . . . 4  |-  (/) : (/) -1-1-onto-> (/)
27 ennnfonelemh.dceq . . . . . 6  |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
28 ennnfonelemh.f . . . . . 6  |-  ( ph  ->  F : om -onto-> A
)
29 ennnfonelemh.ne . . . . . 6  |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
30 ennnfonelemh.g . . . . . 6  |-  G  =  ( x  e.  ( A  ^pm  om ) ,  y  e.  om  |->  if ( ( F `  y )  e.  ( F " y ) ,  x ,  ( x  u.  { <. dom  x ,  ( F `
 y ) >. } ) ) )
31 ennnfonelemh.n . . . . . 6  |-  N  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
32 ennnfonelemh.j . . . . . 6  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
33 ennnfonelemh.h . . . . . 6  |-  H  =  seq 0 ( G ,  J )
3427, 28, 29, 30, 31, 32, 33ennnfonelem0 12419 . . . . 5  |-  ( ph  ->  ( H `  0
)  =  (/) )
3534dmeqd 4841 . . . . . 6  |-  ( ph  ->  dom  ( H ` 
0 )  =  dom  (/) )
36 dm0 4853 . . . . . 6  |-  dom  (/)  =  (/)
3735, 36eqtrdi 2236 . . . . 5  |-  ( ph  ->  dom  ( H ` 
0 )  =  (/) )
38 0zd 9278 . . . . . . . . . . . 12  |-  ( T. 
->  0  e.  ZZ )
3938, 31frec2uz0d 10412 . . . . . . . . . . 11  |-  ( T. 
->  ( N `  (/) )  =  0 )
4039mptru 1372 . . . . . . . . . 10  |-  ( N `
 (/) )  =  0
4140fveq2i 5530 . . . . . . . . 9  |-  ( `' N `  ( N `
 (/) ) )  =  ( `' N ` 
0 )
4238, 31frec2uzf1od 10419 . . . . . . . . . . 11  |-  ( T. 
->  N : om -1-1-onto-> ( ZZ>= `  0 )
)
4342mptru 1372 . . . . . . . . . 10  |-  N : om
-1-1-onto-> ( ZZ>= `  0 )
44 peano1 4605 . . . . . . . . . 10  |-  (/)  e.  om
45 f1ocnvfv1 5791 . . . . . . . . . 10  |-  ( ( N : om -1-1-onto-> ( ZZ>= `  0 )  /\  (/)  e.  om )  ->  ( `' N `  ( N `  (/) ) )  =  (/) )
4643, 44, 45mp2an 426 . . . . . . . . 9  |-  ( `' N `  ( N `
 (/) ) )  =  (/)
4741, 46eqtr3i 2210 . . . . . . . 8  |-  ( `' N `  0 )  =  (/)
4847imaeq2i 4980 . . . . . . 7  |-  ( F
" ( `' N `  0 ) )  =  ( F " (/) )
49 ima0 4999 . . . . . . 7  |-  ( F
" (/) )  =  (/)
5048, 49eqtri 2208 . . . . . 6  |-  ( F
" ( `' N `  0 ) )  =  (/)
5150a1i 9 . . . . 5  |-  ( ph  ->  ( F " ( `' N `  0 ) )  =  (/) )
5234, 37, 51f1oeq123d 5467 . . . 4  |-  ( ph  ->  ( ( H ` 
0 ) : dom  ( H `  0 ) -1-1-onto-> ( F " ( `' N `  0 ) )  <->  (/) : (/) -1-1-onto-> (/) ) )
5326, 52mpbiri 168 . . 3  |-  ( ph  ->  ( H `  0
) : dom  ( H `  0 ) -1-1-onto-> ( F " ( `' N `  0 ) ) )
54 simplr 528 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )
5527ad2antrr 488 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y
)
5628ad2antrr 488 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  F : om -onto-> A )
5729ad2antrr 488 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  A. n  e.  om  E. k  e. 
om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )
)
58 simplr 528 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  k  e.  NN0 )
5955, 56, 57, 30, 31, 32, 33, 58ennnfonelemp1 12420 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( H `  ( k  +  1 ) )  =  if ( ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) ,  ( H `  k
) ,  ( ( H `  k )  u.  { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } ) ) )
6059adantr 276 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( H `  ( k  +  1 ) )  =  if ( ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) ,  ( H `  k
) ,  ( ( H `  k )  u.  { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } ) ) )
61 simpr 110 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )
6261iftrued 3553 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  if ( ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) ,  ( H `  k
) ,  ( ( H `  k )  u.  { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } ) )  =  ( H `  k ) )
6360, 62eqtrd 2220 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( H `  ( k  +  1 ) )  =  ( H `  k ) )
6463dmeqd 4841 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  dom  ( H `  ( k  +  1 ) )  =  dom  ( H `  k ) )
65 0zd 9278 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  0  e.  ZZ )
6631frechashgf1o 10441 . . . . . . . . . . . . . . . . . . . . 21  |-  N : om
-1-1-onto-> NN0
6766a1i 9 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  N : om -1-1-onto-> NN0 )
68 f1ocnv 5486 . . . . . . . . . . . . . . . . . . . 20  |-  ( N : om -1-1-onto-> NN0  ->  `' N : NN0
-1-1-onto-> om )
69 f1of 5473 . . . . . . . . . . . . . . . . . . . 20  |-  ( `' N : NN0 -1-1-onto-> om  ->  `' N : NN0 --> om )
7067, 68, 693syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  `' N : NN0 --> om )
7170, 58ffvelcdmd 5665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( `' N `  k )  e.  om )
7265, 31, 71frec2uzsucd 10414 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( N `  suc  ( `' N `  k ) )  =  ( ( N `  ( `' N `  k ) )  +  1 ) )
73 f1ocnvfv2 5792 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N : om -1-1-onto-> NN0  /\  k  e. 
NN0 )  ->  ( N `  ( `' N `  k )
)  =  k )
7466, 58, 73sylancr 414 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( N `  ( `' N `  k )
)  =  k )
7574oveq1d 5903 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  (
( N `  ( `' N `  k ) )  +  1 )  =  ( k  +  1 ) )
7672, 75eqtrd 2220 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( N `  suc  ( `' N `  k ) )  =  ( k  +  1 ) )
7776fveq2d 5531 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( `' N `  ( N `
 suc  ( `' N `  k )
) )  =  ( `' N `  ( k  +  1 ) ) )
78 peano2 4606 . . . . . . . . . . . . . . . . 17  |-  ( ( `' N `  k )  e.  om  ->  suc  ( `' N `  k )  e.  om )
7971, 78syl 14 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  suc  ( `' N `  k )  e.  om )
80 f1ocnvfv1 5791 . . . . . . . . . . . . . . . 16  |-  ( ( N : om -1-1-onto-> NN0  /\  suc  ( `' N `  k )  e.  om )  -> 
( `' N `  ( N `  suc  ( `' N `  k ) ) )  =  suc  ( `' N `  k ) )
8166, 79, 80sylancr 414 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( `' N `  ( N `
 suc  ( `' N `  k )
) )  =  suc  ( `' N `  k ) )
8277, 81eqtr3d 2222 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( `' N `  ( k  +  1 ) )  =  suc  ( `' N `  k ) )
83 df-suc 4383 . . . . . . . . . . . . . 14  |-  suc  ( `' N `  k )  =  ( ( `' N `  k )  u.  { ( `' N `  k ) } )
8482, 83eqtrdi 2236 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( `' N `  ( k  +  1 ) )  =  ( ( `' N `  k )  u.  { ( `' N `  k ) } ) )
8584imaeq2d 4982 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( F " ( `' N `  ( k  +  1 ) ) )  =  ( F " (
( `' N `  k )  u.  {
( `' N `  k ) } ) ) )
86 imaundi 5053 . . . . . . . . . . . 12  |-  ( F
" ( ( `' N `  k )  u.  { ( `' N `  k ) } ) )  =  ( ( F "
( `' N `  k ) )  u.  ( F " {
( `' N `  k ) } ) )
8785, 86eqtrdi 2236 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( F " ( `' N `  ( k  +  1 ) ) )  =  ( ( F "
( `' N `  k ) )  u.  ( F " {
( `' N `  k ) } ) ) )
8887adantr 276 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( F "
( `' N `  ( k  +  1 ) ) )  =  ( ( F "
( `' N `  k ) )  u.  ( F " {
( `' N `  k ) } ) ) )
8961snssd 3749 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  { ( F `
 ( `' N `  k ) ) } 
C_  ( F "
( `' N `  k ) ) )
90 ssequn2 3320 . . . . . . . . . . . 12  |-  ( { ( F `  ( `' N `  k ) ) }  C_  ( F " ( `' N `  k ) )  <->  ( ( F " ( `' N `  k ) )  u. 
{ ( F `  ( `' N `  k ) ) } )  =  ( F " ( `' N `  k ) ) )
9189, 90sylib 122 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( ( F
" ( `' N `  k ) )  u. 
{ ( F `  ( `' N `  k ) ) } )  =  ( F " ( `' N `  k ) ) )
92 fofn 5452 . . . . . . . . . . . . . . . 16  |-  ( F : om -onto-> A  ->  F  Fn  om )
9356, 92syl 14 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  F  Fn  om )
94 fnsnfv 5588 . . . . . . . . . . . . . . 15  |-  ( ( F  Fn  om  /\  ( `' N `  k )  e.  om )  ->  { ( F `  ( `' N `  k ) ) }  =  ( F " { ( `' N `  k ) } ) )
9593, 71, 94syl2anc 411 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  { ( F `  ( `' N `  k ) ) }  =  ( F " { ( `' N `  k ) } ) )
9695uneq2d 3301 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  (
( F " ( `' N `  k ) )  u.  { ( F `  ( `' N `  k ) ) } )  =  ( ( F "
( `' N `  k ) )  u.  ( F " {
( `' N `  k ) } ) ) )
9796eqeq1d 2196 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  (
( ( F "
( `' N `  k ) )  u. 
{ ( F `  ( `' N `  k ) ) } )  =  ( F " ( `' N `  k ) )  <->  ( ( F
" ( `' N `  k ) )  u.  ( F " {
( `' N `  k ) } ) )  =  ( F
" ( `' N `  k ) ) ) )
9897adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( ( ( F " ( `' N `  k ) )  u.  { ( F `  ( `' N `  k ) ) } )  =  ( F " ( `' N `  k ) )  <->  ( ( F
" ( `' N `  k ) )  u.  ( F " {
( `' N `  k ) } ) )  =  ( F
" ( `' N `  k ) ) ) )
9991, 98mpbid 147 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( ( F
" ( `' N `  k ) )  u.  ( F " {
( `' N `  k ) } ) )  =  ( F
" ( `' N `  k ) ) )
10088, 99eqtrd 2220 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( F "
( `' N `  ( k  +  1 ) ) )  =  ( F " ( `' N `  k ) ) )
10163, 64, 100f1oeq123d 5467 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( ( H `
 ( k  +  1 ) ) : dom  ( H `  ( k  +  1 ) ) -1-1-onto-> ( F " ( `' N `  ( k  +  1 ) ) )  <->  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) ) )
10254, 101mpbird 167 . . . . . . 7  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )  ->  ( H `  ( k  +  1 ) ) : dom  ( H `  ( k  +  1 ) ) -1-1-onto-> ( F " ( `' N `  ( k  +  1 ) ) ) )
103 simplr 528 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )
10455, 56, 57, 30, 31, 32, 33, 58ennnfonelemom 12422 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  dom  ( H `  k )  e.  om )
105104adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  dom  ( H `  k )  e.  om )
106 fof 5450 . . . . . . . . . . . . . 14  |-  ( F : om -onto-> A  ->  F : om --> A )
10756, 106syl 14 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  F : om --> A )
108107, 71ffvelcdmd 5665 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( F `  ( `' N `  k )
)  e.  A )
109108adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  ( F `  ( `' N `  k )
)  e.  A )
110 f1osng 5514 . . . . . . . . . . 11  |-  ( ( dom  ( H `  k )  e.  om  /\  ( F `  ( `' N `  k ) )  e.  A )  ->  { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } : { dom  ( H `  k
) } -1-1-onto-> { ( F `  ( `' N `  k ) ) } )
111105, 109, 110syl2anc 411 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  { <. dom  ( H `  k
) ,  ( F `
 ( `' N `  k ) ) >. } : { dom  ( H `  k ) }
-1-1-onto-> { ( F `  ( `' N `  k ) ) } )
11295adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  { ( F `  ( `' N `  k ) ) }  =  ( F " { ( `' N `  k ) } ) )
113 f1oeq3 5463 . . . . . . . . . . 11  |-  ( { ( F `  ( `' N `  k ) ) }  =  ( F " { ( `' N `  k ) } )  ->  ( { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } : { dom  ( H `  k
) } -1-1-onto-> { ( F `  ( `' N `  k ) ) }  <->  { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } : { dom  ( H `  k
) } -1-1-onto-> ( F " {
( `' N `  k ) } ) ) )
114112, 113syl 14 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  ( { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } : { dom  ( H `  k
) } -1-1-onto-> { ( F `  ( `' N `  k ) ) }  <->  { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } : { dom  ( H `  k
) } -1-1-onto-> ( F " {
( `' N `  k ) } ) ) )
115111, 114mpbid 147 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  { <. dom  ( H `  k
) ,  ( F `
 ( `' N `  k ) ) >. } : { dom  ( H `  k ) }
-1-1-onto-> ( F " { ( `' N `  k ) } ) )
116 nnord 4623 . . . . . . . . . 10  |-  ( dom  ( H `  k
)  e.  om  ->  Ord 
dom  ( H `  k ) )
117 orddisj 4557 . . . . . . . . . 10  |-  ( Ord 
dom  ( H `  k )  ->  ( dom  ( H `  k
)  i^i  { dom  ( H `  k ) } )  =  (/) )
118105, 116, 1173syl 17 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  ( dom  ( H `  k
)  i^i  { dom  ( H `  k ) } )  =  (/) )
119112ineq2d 3348 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  (
( F " ( `' N `  k ) )  i^i  { ( F `  ( `' N `  k ) ) } )  =  ( ( F "
( `' N `  k ) )  i^i  ( F " {
( `' N `  k ) } ) ) )
120 simpr 110 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  -.  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )
121 disjsn 3666 . . . . . . . . . . 11  |-  ( ( ( F " ( `' N `  k ) )  i^i  { ( F `  ( `' N `  k ) ) } )  =  (/) 
<->  -.  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )
122120, 121sylibr 134 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  (
( F " ( `' N `  k ) )  i^i  { ( F `  ( `' N `  k ) ) } )  =  (/) )
123119, 122eqtr3d 2222 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  (
( F " ( `' N `  k ) )  i^i  ( F
" { ( `' N `  k ) } ) )  =  (/) )
124 f1oun 5493 . . . . . . . . 9  |-  ( ( ( ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) )  /\  { <. dom  ( H `  k
) ,  ( F `
 ( `' N `  k ) ) >. } : { dom  ( H `  k ) }
-1-1-onto-> ( F " { ( `' N `  k ) } ) )  /\  ( ( dom  ( H `  k )  i^i  { dom  ( H `
 k ) } )  =  (/)  /\  (
( F " ( `' N `  k ) )  i^i  ( F
" { ( `' N `  k ) } ) )  =  (/) ) )  ->  (
( H `  k
)  u.  { <. dom  ( H `  k
) ,  ( F `
 ( `' N `  k ) ) >. } ) : ( dom  ( H `  k )  u.  { dom  ( H `  k
) } ) -1-1-onto-> ( ( F " ( `' N `  k ) )  u.  ( F
" { ( `' N `  k ) } ) ) )
125103, 115, 118, 123, 124syl22anc 1249 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  (
( H `  k
)  u.  { <. dom  ( H `  k
) ,  ( F `
 ( `' N `  k ) ) >. } ) : ( dom  ( H `  k )  u.  { dom  ( H `  k
) } ) -1-1-onto-> ( ( F " ( `' N `  k ) )  u.  ( F
" { ( `' N `  k ) } ) ) )
12659adantr 276 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  ( H `  ( k  +  1 ) )  =  if ( ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) ,  ( H `  k
) ,  ( ( H `  k )  u.  { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } ) ) )
127120iffalsed 3556 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  if ( ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) ,  ( H `  k
) ,  ( ( H `  k )  u.  { <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } ) )  =  ( ( H `
 k )  u. 
{ <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } ) )
128126, 127eqtrd 2220 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  ( H `  ( k  +  1 ) )  =  ( ( H `
 k )  u. 
{ <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } ) )
12955adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y
)
13056adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  F : om -onto-> A )
13157adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  A. n  e.  om  E. k  e. 
om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )
)
13258adantr 276 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  k  e.  NN0 )
133129, 130, 131, 30, 31, 32, 33, 132, 120ennnfonelemhdmp1 12423 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  dom  ( H `  ( k  +  1 ) )  =  suc  dom  ( H `  k )
)
134 df-suc 4383 . . . . . . . . . 10  |-  suc  dom  ( H `  k )  =  ( dom  ( H `  k )  u.  { dom  ( H `
 k ) } )
135133, 134eqtrdi 2236 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  dom  ( H `  ( k  +  1 ) )  =  ( dom  ( H `  k )  u.  { dom  ( H `
 k ) } ) )
13687adantr 276 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  ( F " ( `' N `  ( k  +  1 ) ) )  =  ( ( F "
( `' N `  k ) )  u.  ( F " {
( `' N `  k ) } ) ) )
137128, 135, 136f1oeq123d 5467 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  (
( H `  (
k  +  1 ) ) : dom  ( H `  ( k  +  1 ) ) -1-1-onto-> ( F " ( `' N `  ( k  +  1 ) ) )  <->  ( ( H `
 k )  u. 
{ <. dom  ( H `  k ) ,  ( F `  ( `' N `  k ) ) >. } ) : ( dom  ( H `
 k )  u. 
{ dom  ( H `  k ) } ) -1-1-onto-> ( ( F " ( `' N `  k ) )  u.  ( F
" { ( `' N `  k ) } ) ) ) )
138125, 137mpbird 167 . . . . . . 7  |-  ( ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `
 k ) -1-1-onto-> ( F
" ( `' N `  k ) ) )  /\  -.  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) ) )  ->  ( H `  ( k  +  1 ) ) : dom  ( H `
 ( k  +  1 ) ) -1-1-onto-> ( F
" ( `' N `  ( k  +  1 ) ) ) )
13955, 56, 71ennnfonelemdc 12413 . . . . . . . 8  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  -> DECID  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) )
140 exmiddc 837 . . . . . . . 8  |-  (DECID  ( F `
 ( `' N `  k ) )  e.  ( F " ( `' N `  k ) )  ->  ( ( F `  ( `' N `  k )
)  e.  ( F
" ( `' N `  k ) )  \/ 
-.  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) ) )
141139, 140syl 14 . . . . . . 7  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  (
( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) )  \/ 
-.  ( F `  ( `' N `  k ) )  e.  ( F
" ( `' N `  k ) ) ) )
142102, 138, 141mpjaodan 799 . . . . . 6  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( H `  ( k  +  1 ) ) : dom  ( H `
 ( k  +  1 ) ) -1-1-onto-> ( F
" ( `' N `  ( k  +  1 ) ) ) )
143142ex 115 . . . . 5  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) )  ->  ( H `  ( k  +  1 ) ) : dom  ( H `  ( k  +  1 ) ) -1-1-onto-> ( F " ( `' N `  ( k  +  1 ) ) ) ) )
144143expcom 116 . . . 4  |-  ( k  e.  NN0  ->  ( ph  ->  ( ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) )  ->  ( H `  ( k  +  1 ) ) : dom  ( H `  ( k  +  1 ) ) -1-1-onto-> ( F " ( `' N `  ( k  +  1 ) ) ) ) ) )
145144a2d 26 . . 3  |-  ( k  e.  NN0  ->  ( (
ph  ->  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( ph  ->  ( H `  ( k  +  1 ) ) : dom  ( H `  ( k  +  1 ) ) -1-1-onto-> ( F " ( `' N `  ( k  +  1 ) ) ) ) ) )
1467, 13, 19, 25, 53, 145nn0ind 9380 . 2  |-  ( P  e.  NN0  ->  ( ph  ->  ( H `  P
) : dom  ( H `  P ) -1-1-onto-> ( F " ( `' N `  P ) ) ) )
1471, 146mpcom 36 1  |-  ( ph  ->  ( H `  P
) : dom  ( H `  P ) -1-1-onto-> ( F " ( `' N `  P ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 709  DECID wdc 835    = wceq 1363   T. wtru 1364    e. wcel 2158    =/= wne 2357   A.wral 2465   E.wrex 2466    u. cun 3139    i^i cin 3140    C_ wss 3141   (/)c0 3434   ifcif 3546   {csn 3604   <.cop 3607    |-> cmpt 4076   Ord word 4374   suc csuc 4377   omcom 4601   `'ccnv 4637   dom cdm 4638   "cima 4641    Fn wfn 5223   -->wf 5224   -onto->wfo 5226   -1-1-onto->wf1o 5227   ` cfv 5228  (class class class)co 5888    e. cmpo 5890  freccfrec 6404    ^pm cpm 6662   0cc0 7824   1c1 7825    + caddc 7827    - cmin 8141   NN0cn0 9189   ZZcz 9266   ZZ>=cuz 9541    seqcseq 10458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-addcom 7924  ax-addass 7926  ax-distr 7928  ax-i2m1 7929  ax-0lt1 7930  ax-0id 7932  ax-rnegex 7933  ax-cnre 7935  ax-pre-ltirr 7936  ax-pre-ltwlin 7937  ax-pre-lttrn 7938  ax-pre-ltadd 7940
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-if 3547  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-id 4305  df-iord 4378  df-on 4380  df-ilim 4381  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-frec 6405  df-pm 6664  df-pnf 8007  df-mnf 8008  df-xr 8009  df-ltxr 8010  df-le 8011  df-sub 8143  df-neg 8144  df-inn 8933  df-n0 9190  df-z 9267  df-uz 9542  df-seqfrec 10459
This theorem is referenced by:  ennnfonelemex  12428  ennnfonelemf1  12432  ennnfonelemrn  12433
  Copyright terms: Public domain W3C validator