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

Theorem ennnfonelemhf1o 12394
Description: Lemma for ennnfone 12406. 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 5511 . . . . 5  |-  ( w  =  0  ->  ( H `  w )  =  ( H ` 
0 ) )
32dmeqd 4825 . . . . 5  |-  ( w  =  0  ->  dom  ( H `  w )  =  dom  ( H `
 0 ) )
4 fveq2 5511 . . . . . 6  |-  ( w  =  0  ->  ( `' N `  w )  =  ( `' N `  0 ) )
54imaeq2d 4966 . . . . 5  |-  ( w  =  0  ->  ( F " ( `' N `  w ) )  =  ( F " ( `' N `  0 ) ) )
62, 3, 5f1oeq123d 5451 . . . 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 5511 . . . . 5  |-  ( w  =  k  ->  ( H `  w )  =  ( H `  k ) )
98dmeqd 4825 . . . . 5  |-  ( w  =  k  ->  dom  ( H `  w )  =  dom  ( H `
 k ) )
10 fveq2 5511 . . . . . 6  |-  ( w  =  k  ->  ( `' N `  w )  =  ( `' N `  k ) )
1110imaeq2d 4966 . . . . 5  |-  ( w  =  k  ->  ( F " ( `' N `  w ) )  =  ( F " ( `' N `  k ) ) )
128, 9, 11f1oeq123d 5451 . . . 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 5511 . . . . 5  |-  ( w  =  ( k  +  1 )  ->  ( H `  w )  =  ( H `  ( k  +  1 ) ) )
1514dmeqd 4825 . . . . 5  |-  ( w  =  ( k  +  1 )  ->  dom  ( H `  w )  =  dom  ( H `
 ( k  +  1 ) ) )
16 fveq2 5511 . . . . . 6  |-  ( w  =  ( k  +  1 )  ->  ( `' N `  w )  =  ( `' N `  ( k  +  1 ) ) )
1716imaeq2d 4966 . . . . 5  |-  ( w  =  ( k  +  1 )  ->  ( F " ( `' N `  w ) )  =  ( F " ( `' N `  ( k  +  1 ) ) ) )
1814, 15, 17f1oeq123d 5451 . . . 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 5511 . . . . 5  |-  ( w  =  P  ->  ( H `  w )  =  ( H `  P ) )
2120dmeqd 4825 . . . . 5  |-  ( w  =  P  ->  dom  ( H `  w )  =  dom  ( H `
 P ) )
22 fveq2 5511 . . . . . 6  |-  ( w  =  P  ->  ( `' N `  w )  =  ( `' N `  P ) )
2322imaeq2d 4966 . . . . 5  |-  ( w  =  P  ->  ( F " ( `' N `  w ) )  =  ( F " ( `' N `  P ) ) )
2420, 21, 23f1oeq123d 5451 . . . 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 5494 . . . 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 12386 . . . . 5  |-  ( ph  ->  ( H `  0
)  =  (/) )
3534dmeqd 4825 . . . . . 6  |-  ( ph  ->  dom  ( H ` 
0 )  =  dom  (/) )
36 dm0 4837 . . . . . 6  |-  dom  (/)  =  (/)
3735, 36eqtrdi 2226 . . . . 5  |-  ( ph  ->  dom  ( H ` 
0 )  =  (/) )
38 0zd 9251 . . . . . . . . . . . 12  |-  ( T. 
->  0  e.  ZZ )
3938, 31frec2uz0d 10382 . . . . . . . . . . 11  |-  ( T. 
->  ( N `  (/) )  =  0 )
4039mptru 1362 . . . . . . . . . 10  |-  ( N `
 (/) )  =  0
4140fveq2i 5514 . . . . . . . . 9  |-  ( `' N `  ( N `
 (/) ) )  =  ( `' N ` 
0 )
4238, 31frec2uzf1od 10389 . . . . . . . . . . 11  |-  ( T. 
->  N : om -1-1-onto-> ( ZZ>= `  0 )
)
4342mptru 1362 . . . . . . . . . 10  |-  N : om
-1-1-onto-> ( ZZ>= `  0 )
44 peano1 4590 . . . . . . . . . 10  |-  (/)  e.  om
45 f1ocnvfv1 5772 . . . . . . . . . 10  |-  ( ( N : om -1-1-onto-> ( ZZ>= `  0 )  /\  (/)  e.  om )  ->  ( `' N `  ( N `  (/) ) )  =  (/) )
4643, 44, 45mp2an 426 . . . . . . . . 9  |-  ( `' N `  ( N `
 (/) ) )  =  (/)
4741, 46eqtr3i 2200 . . . . . . . 8  |-  ( `' N `  0 )  =  (/)
4847imaeq2i 4964 . . . . . . 7  |-  ( F
" ( `' N `  0 ) )  =  ( F " (/) )
49 ima0 4983 . . . . . . 7  |-  ( F
" (/) )  =  (/)
5048, 49eqtri 2198 . . . . . 6  |-  ( F
" ( `' N `  0 ) )  =  (/)
5150a1i 9 . . . . 5  |-  ( ph  ->  ( F " ( `' N `  0 ) )  =  (/) )
5234, 37, 51f1oeq123d 5451 . . . 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 12387 . . . . . . . . . . 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 3541 . . . . . . . . . 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 2210 . . . . . . . . 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 4825 . . . . . . . . 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 9251 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  0  e.  ZZ )
6631frechashgf1o 10411 . . . . . . . . . . . . . . . . . . . . 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 5470 . . . . . . . . . . . . . . . . . . . 20  |-  ( N : om -1-1-onto-> NN0  ->  `' N : NN0
-1-1-onto-> om )
69 f1of 5457 . . . . . . . . . . . . . . . . . . . 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 5648 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( `' N `  k )  e.  om )
7265, 31, 71frec2uzsucd 10384 . . . . . . . . . . . . . . . . 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 5773 . . . . . . . . . . . . . . . . . . 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 5884 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  (
( N `  ( `' N `  k ) )  +  1 )  =  ( k  +  1 ) )
7672, 75eqtrd 2210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  NN0 )  /\  ( H `  k ) : dom  ( H `  k ) -1-1-onto-> ( F " ( `' N `  k ) ) )  ->  ( N `  suc  ( `' N `  k ) )  =  ( k  +  1 ) )
7776fveq2d 5515 . . . . . . . . . . . . . . 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 4591 . . . . . . . . . . . . . . . . 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 5772 . . . . . . . . . . . . . . . 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 2212 . . . . . . . . . . . . . 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 4368 . . . . . . . . . . . . . 14  |-  suc  ( `' N `  k )  =  ( ( `' N `  k )  u.  { ( `' N `  k ) } )
8482, 83eqtrdi 2226 . . . . . . . . . . . . 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 4966 . . . . . . . . . . . 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 5037 . . . . . . . . . . . 12  |-  ( F
" ( ( `' N `  k )  u.  { ( `' N `  k ) } ) )  =  ( ( F "
( `' N `  k ) )  u.  ( F " {
( `' N `  k ) } ) )
8785, 86eqtrdi 2226 . . . . . . . . . . 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 3736 . . . . . . . . . . . 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 3308 . . . . . . . . . . . 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 5436 . . . . . . . . . . . . . . . 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 5571 . . . . . . . . . . . . . . 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 3289 . . . . . . . . . . . . 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 2186 . . . . . . . . . . . 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 2210 . . . . . . . . 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 5451 . . . . . . . 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 12389 . . . . . . . . . . . 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 5434 . . . . . . . . . . . . . 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 5648 . . . . . . . . . . . 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 5498 . . . . . . . . . . 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 5447 . . . . . . . . . . 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 4608 . . . . . . . . . 10  |-  ( dom  ( H `  k
)  e.  om  ->  Ord 
dom  ( H `  k ) )
117 orddisj 4542 . . . . . . . . . 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 3336 . . . . . . . . . 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 3653 . . . . . . . . . . 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 2212 . . . . . . . . 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 5477 . . . . . . . . 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 1239 . . . . . . . 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 3544 . . . . . . . . . 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 2210 . . . . . . . . 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 12390 . . . . . . . . . 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 4368 . . . . . . . . . 10  |-  suc  dom  ( H `  k )  =  ( dom  ( H `  k )  u.  { dom  ( H `
 k ) } )
135133, 134eqtrdi 2226 . . . . . . . . 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 5451 . . . . . . . 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 12380 . . . . . . . 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 836 . . . . . . . 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 798 . . . . . 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 9353 . 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 708  DECID wdc 834    = wceq 1353   T. wtru 1354    e. wcel 2148    =/= wne 2347   A.wral 2455   E.wrex 2456    u. cun 3127    i^i cin 3128    C_ wss 3129   (/)c0 3422   ifcif 3534   {csn 3591   <.cop 3594    |-> cmpt 4061   Ord word 4359   suc csuc 4362   omcom 4586   `'ccnv 4622   dom cdm 4623   "cima 4626    Fn wfn 5207   -->wf 5208   -onto->wfo 5210   -1-1-onto->wf1o 5211   ` cfv 5212  (class class class)co 5869    e. cmpo 5871  freccfrec 6385    ^pm cpm 6643   0cc0 7799   1c1 7800    + caddc 7802    - cmin 8115   NN0cn0 9162   ZZcz 9239   ZZ>=cuz 9514    seqcseq 10428
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-nul 4126  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-iinf 4584  ax-cnex 7890  ax-resscn 7891  ax-1cn 7892  ax-1re 7893  ax-icn 7894  ax-addcl 7895  ax-addrcl 7896  ax-mulcl 7897  ax-addcom 7899  ax-addass 7901  ax-distr 7903  ax-i2m1 7904  ax-0lt1 7905  ax-0id 7907  ax-rnegex 7908  ax-cnre 7910  ax-pre-ltirr 7911  ax-pre-ltwlin 7912  ax-pre-lttrn 7913  ax-pre-ltadd 7915
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-tr 4099  df-id 4290  df-iord 4363  df-on 4365  df-ilim 4366  df-suc 4368  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-recs 6300  df-frec 6386  df-pm 6645  df-pnf 7981  df-mnf 7982  df-xr 7983  df-ltxr 7984  df-le 7985  df-sub 8117  df-neg 8118  df-inn 8906  df-n0 9163  df-z 9240  df-uz 9515  df-seqfrec 10429
This theorem is referenced by:  ennnfonelemex  12395  ennnfonelemf1  12399  ennnfonelemrn  12400
  Copyright terms: Public domain W3C validator