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

Theorem ennnfonelemex 12369
Description: Lemma for ennnfone 12380. Extending the sequence  ( H `  P ) to include an additional element. (Contributed by Jim Kingdon, 19-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 )
ennnfonelemex.p  |-  ( ph  ->  P  e.  NN0 )
Assertion
Ref Expression
ennnfonelemex  |-  ( ph  ->  E. i  e.  NN0  dom  ( H `  P
)  e.  dom  ( H `  i )
)
Distinct variable groups:    A, j, x, y    j, F, k, n    x, F, y   
j, G    j, H, k, n    i, H, k   
x, H, y, k   
j, J    j, N, k, n    i, N    x, N, y    P, j, k, n    x, P, y    P, i    ph, j, k, n    ph, x, y
Allowed substitution hints:    ph( i)    A( i,
k, n)    F( i)    G( x, y, i, k, n)    J( x, y, i, k, n)

Proof of Theorem ennnfonelemex
Dummy variables  a  b  q  s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suceq 4387 . . . . 5  |-  ( n  =  ( `' N `  P )  ->  suc  n  =  suc  ( `' N `  P ) )
21raleqdv 2671 . . . 4  |-  ( n  =  ( `' N `  P )  ->  ( A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )
32rexbidv 2471 . . 3  |-  ( n  =  ( `' N `  P )  ->  ( E. k  e.  om  A. j  e.  suc  n
( F `  k
)  =/=  ( F `
 j )  <->  E. k  e.  om  A. j  e. 
suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )
4 ennnfonelemh.ne . . 3  |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
5 ennnfonelemh.n . . . . . . 7  |-  N  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
65frechashgf1o 10384 . . . . . 6  |-  N : om
-1-1-onto-> NN0
7 f1ocnv 5455 . . . . . 6  |-  ( N : om -1-1-onto-> NN0  ->  `' N : NN0
-1-1-onto-> om )
86, 7ax-mp 5 . . . . 5  |-  `' N : NN0
-1-1-onto-> om
9 f1of 5442 . . . . 5  |-  ( `' N : NN0 -1-1-onto-> om  ->  `' N : NN0 --> om )
108, 9mp1i 10 . . . 4  |-  ( ph  ->  `' N : NN0 --> om )
11 ennnfonelemex.p . . . 4  |-  ( ph  ->  P  e.  NN0 )
1210, 11ffvelrnd 5632 . . 3  |-  ( ph  ->  ( `' N `  P )  e.  om )
133, 4, 12rspcdva 2839 . 2  |-  ( ph  ->  E. k  e.  om  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) )
14 f1of 5442 . . . . 5  |-  ( N : om -1-1-onto-> NN0  ->  N : om
--> NN0 )
156, 14mp1i 10 . . . 4  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  N : om --> NN0 )
16 peano2 4579 . . . . 5  |-  ( k  e.  om  ->  suc  k  e.  om )
1716ad2antrl 487 . . . 4  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  suc  k  e.  om )
1815, 17ffvelrnd 5632 . . 3  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  suc  k )  e.  NN0 )
19 ennnfonelemh.f . . . . . . . . 9  |-  ( ph  ->  F : om -onto-> A
)
2019ad2antrr 485 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  ->  F : om -onto-> A )
21 fofun 5421 . . . . . . . 8  |-  ( F : om -onto-> A  ->  Fun  F )
2220, 21syl 14 . . . . . . 7  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  ->  Fun  F )
23 vex 2733 . . . . . . . . . 10  |-  k  e. 
_V
2423sucid 4402 . . . . . . . . 9  |-  k  e. 
suc  k
25 simprl 526 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
k  e.  om )
2625adantr 274 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  -> 
k  e.  om )
27 fof 5420 . . . . . . . . . . . 12  |-  ( F : om -onto-> A  ->  F : om --> A )
28 fdm 5353 . . . . . . . . . . . 12  |-  ( F : om --> A  ->  dom  F  =  om )
2920, 27, 283syl 17 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  ->  dom  F  =  om )
3026, 29eleqtrrd 2250 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  -> 
k  e.  dom  F
)
31 funfvima 5727 . . . . . . . . . 10  |-  ( ( Fun  F  /\  k  e.  dom  F )  -> 
( k  e.  suc  k  ->  ( F `  k )  e.  ( F " suc  k
) ) )
3222, 30, 31syl2anc 409 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  -> 
( k  e.  suc  k  ->  ( F `  k )  e.  ( F " suc  k
) ) )
3324, 32mpi 15 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  -> 
( F `  k
)  e.  ( F
" suc  k )
)
34 simpr 109 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  ->  dom  ( H `  P
)  =  dom  ( H `  ( N `  suc  k ) ) )
35 ennnfonelemh.dceq . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
3635adantr 274 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
3719adantr 274 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  F : om -onto-> A )
384adantr 274 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
39 fveq2 5496 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  a  ->  ( F `  j )  =  ( F `  a ) )
4039neeq2d 2359 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  a  ->  (
( F `  k
)  =/=  ( F `
 j )  <->  ( F `  k )  =/=  ( F `  a )
) )
4140cbvralv 2696 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  A. a  e.  suc  n ( F `
 k )  =/=  ( F `  a
) )
4241rexbii 2477 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  E. k  e.  om  A. a  e. 
suc  n ( F `
 k )  =/=  ( F `  a
) )
43 fveq2 5496 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  b  ->  ( F `  k )  =  ( F `  b ) )
4443neeq1d 2358 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  b  ->  (
( F `  k
)  =/=  ( F `
 a )  <->  ( F `  b )  =/=  ( F `  a )
) )
4544ralbidv 2470 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  b  ->  ( A. a  e.  suc  n ( F `  k )  =/=  ( F `  a )  <->  A. a  e.  suc  n
( F `  b
)  =/=  ( F `
 a ) ) )
4645cbvrexv 2697 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. k  e.  om  A. a  e.  suc  n ( F `  k )  =/=  ( F `  a )  <->  E. b  e.  om  A. a  e. 
suc  n ( F `
 b )  =/=  ( F `  a
) )
4742, 46bitri 183 . . . . . . . . . . . . . . . . . . 19  |-  ( E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  E. b  e.  om  A. a  e. 
suc  n ( F `
 b )  =/=  ( F `  a
) )
4847ralbii 2476 . . . . . . . . . . . . . . . . . 18  |-  ( A. n  e.  om  E. k  e.  om  A. j  e. 
suc  n ( F `
 k )  =/=  ( F `  j
)  <->  A. n  e.  om  E. b  e.  om  A. a  e.  suc  n ( F `  b )  =/=  ( F `  a ) )
4938, 48sylib 121 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  A. n  e.  om  E. b  e.  om  A. a  e.  suc  n ( F `  b )  =/=  ( F `  a ) )
50 ennnfonelemh.g . . . . . . . . . . . . . . . . 17  |-  G  =  ( x  e.  ( A  ^pm  om ) ,  y  e.  om  |->  if ( ( F `  y )  e.  ( F " y ) ,  x ,  ( x  u.  { <. dom  x ,  ( F `
 y ) >. } ) ) )
51 ennnfonelemh.j . . . . . . . . . . . . . . . . 17  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
52 ennnfonelemh.h . . . . . . . . . . . . . . . . 17  |-  H  =  seq 0 ( G ,  J )
5336, 37, 49, 50, 5, 51, 52, 18ennnfonelemhf1o 12368 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( H `  ( N `  suc  k ) ) : dom  ( H `  ( N `  suc  k ) ) -1-1-onto-> ( F " ( `' N `  ( N `
 suc  k )
) ) )
54 f1ofun 5444 . . . . . . . . . . . . . . . 16  |-  ( ( H `  ( N `
 suc  k )
) : dom  ( H `  ( N `  suc  k ) ) -1-1-onto-> ( F " ( `' N `  ( N `
 suc  k )
) )  ->  Fun  ( H `  ( N `
 suc  k )
) )
5553, 54syl 14 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  Fun  ( H `  ( N `  suc  k ) ) )
5655ad2antrr 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  s  e.  dom  ( H `
 P ) )  ->  Fun  ( H `  ( N `  suc  k ) ) )
5711adantr 274 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  P  e.  NN0 )
586, 14mp1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  om )  ->  N : om
--> NN0 )
5916adantl 275 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  om )  ->  suc  k  e. 
om )
6058, 59ffvelrnd 5632 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  om )  ->  ( N `  suc  k )  e. 
NN0 )
6160adantrr 476 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  suc  k )  e.  NN0 )
6257nn0red 9189 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  P  e.  RR )
6361nn0red 9189 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  suc  k )  e.  RR )
64 f1ocnvfv2 5757 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N : om -1-1-onto-> NN0  /\  P  e. 
NN0 )  ->  ( N `  ( `' N `  P )
)  =  P )
656, 57, 64sylancr 412 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  ( `' N `  P ) )  =  P )
6612adantr 274 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( `' N `  P )  e.  om )
67 simprr 527 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) )
6837, 25, 66, 67ennnfonelemk 12355 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( `' N `  P )  e.  k )
69 elelsuc 4394 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( `' N `  P )  e.  k  ->  ( `' N `  P )  e.  suc  k )
7068, 69syl 14 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( `' N `  P )  e.  suc  k )
71 0zd 9224 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
0  e.  ZZ )
7271, 5, 66, 17frec2uzltd 10359 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( ( `' N `  P )  e.  suc  k  ->  ( N `  ( `' N `  P ) )  <  ( N `
 suc  k )
) )
7370, 72mpd 13 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  ( `' N `  P ) )  <  ( N `
 suc  k )
)
7465, 73eqbrtrrd 4013 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  P  <  ( N `  suc  k ) )
7562, 63, 74ltled 8038 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  P  <_  ( N `  suc  k ) )
7636, 37, 38, 50, 5, 51, 52, 57, 61, 75ennnfoneleminc 12366 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( H `  P
)  C_  ( H `  ( N `  suc  k ) ) )
7776ad2antrr 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  s  e.  dom  ( H `
 P ) )  ->  ( H `  P )  C_  ( H `  ( N `  suc  k ) ) )
78 simpr 109 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  s  e.  dom  ( H `
 P ) )  ->  s  e.  dom  ( H `  P ) )
79 funssfv 5522 . . . . . . . . . . . . . 14  |-  ( ( Fun  ( H `  ( N `  suc  k
) )  /\  ( H `  P )  C_  ( H `  ( N `  suc  k ) )  /\  s  e. 
dom  ( H `  P ) )  -> 
( ( H `  ( N `  suc  k
) ) `  s
)  =  ( ( H `  P ) `
 s ) )
8056, 77, 78, 79syl3anc 1233 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  s  e.  dom  ( H `
 P ) )  ->  ( ( H `
 ( N `  suc  k ) ) `  s )  =  ( ( H `  P
) `  s )
)
8180eqcomd 2176 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  s  e.  dom  ( H `
 P ) )  ->  ( ( H `
 P ) `  s )  =  ( ( H `  ( N `  suc  k ) ) `  s ) )
8281ralrimiva 2543 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  ->  A. s  e.  dom  ( H `  P ) ( ( H `  P ) `  s
)  =  ( ( H `  ( N `
 suc  k )
) `  s )
)
8336, 37, 49, 50, 5, 51, 52, 57ennnfonelemhf1o 12368 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( H `  P
) : dom  ( H `  P ) -1-1-onto-> ( F " ( `' N `  P ) ) )
84 f1ofun 5444 . . . . . . . . . . . . . 14  |-  ( ( H `  P ) : dom  ( H `
 P ) -1-1-onto-> ( F
" ( `' N `  P ) )  ->  Fun  ( H `  P
) )
8583, 84syl 14 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  Fun  ( H `  P
) )
86 eqfunfv 5598 . . . . . . . . . . . . 13  |-  ( ( Fun  ( H `  P )  /\  Fun  ( H `  ( N `
 suc  k )
) )  ->  (
( H `  P
)  =  ( H `
 ( N `  suc  k ) )  <->  ( dom  ( H `  P )  =  dom  ( H `
 ( N `  suc  k ) )  /\  A. s  e.  dom  ( H `  P )
( ( H `  P ) `  s
)  =  ( ( H `  ( N `
 suc  k )
) `  s )
) ) )
8785, 55, 86syl2anc 409 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( ( H `  P )  =  ( H `  ( N `
 suc  k )
)  <->  ( dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) )  /\  A. s  e.  dom  ( H `
 P ) ( ( H `  P
) `  s )  =  ( ( H `
 ( N `  suc  k ) ) `  s ) ) ) )
8887adantr 274 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  -> 
( ( H `  P )  =  ( H `  ( N `
 suc  k )
)  <->  ( dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) )  /\  A. s  e.  dom  ( H `
 P ) ( ( H `  P
) `  s )  =  ( ( H `
 ( N `  suc  k ) ) `  s ) ) ) )
8934, 82, 88mpbir2and 939 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  -> 
( H `  P
)  =  ( H `
 ( N `  suc  k ) ) )
9089rneqd 4840 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  ->  ran  ( H `  P
)  =  ran  ( H `  ( N `  suc  k ) ) )
91 dff1o5 5451 . . . . . . . . . . . 12  |-  ( ( H `  P ) : dom  ( H `
 P ) -1-1-onto-> ( F
" ( `' N `  P ) )  <->  ( ( H `  P ) : dom  ( H `  P ) -1-1-> ( F
" ( `' N `  P ) )  /\  ran  ( H `  P
)  =  ( F
" ( `' N `  P ) ) ) )
9283, 91sylib 121 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( ( H `  P ) : dom  ( H `  P )
-1-1-> ( F " ( `' N `  P ) )  /\  ran  ( H `  P )  =  ( F "
( `' N `  P ) ) ) )
9392simprd 113 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  ran  ( H `  P
)  =  ( F
" ( `' N `  P ) ) )
9493adantr 274 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  ->  ran  ( H `  P
)  =  ( F
" ( `' N `  P ) ) )
95 f1ocnvfv1 5756 . . . . . . . . . . . . . . . 16  |-  ( ( N : om -1-1-onto-> NN0  /\  suc  k  e.  om )  ->  ( `' N `  ( N `
 suc  k )
)  =  suc  k
)
966, 17, 95sylancr 412 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( `' N `  ( N `  suc  k
) )  =  suc  k )
9796imaeq2d 4953 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( F " ( `' N `  ( N `
 suc  k )
) )  =  ( F " suc  k
) )
98 f1oeq3 5433 . . . . . . . . . . . . . 14  |-  ( ( F " ( `' N `  ( N `
 suc  k )
) )  =  ( F " suc  k
)  ->  ( ( H `  ( N `  suc  k ) ) : dom  ( H `
 ( N `  suc  k ) ) -1-1-onto-> ( F
" ( `' N `  ( N `  suc  k ) ) )  <-> 
( H `  ( N `  suc  k ) ) : dom  ( H `  ( N `  suc  k ) ) -1-1-onto-> ( F " suc  k
) ) )
9997, 98syl 14 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( ( H `  ( N `  suc  k
) ) : dom  ( H `  ( N `
 suc  k )
)
-1-1-onto-> ( F " ( `' N `  ( N `
 suc  k )
) )  <->  ( H `  ( N `  suc  k ) ) : dom  ( H `  ( N `  suc  k
) ) -1-1-onto-> ( F " suc  k ) ) )
10053, 99mpbid 146 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( H `  ( N `  suc  k ) ) : dom  ( H `  ( N `  suc  k ) ) -1-1-onto-> ( F " suc  k
) )
101 dff1o5 5451 . . . . . . . . . . . 12  |-  ( ( H `  ( N `
 suc  k )
) : dom  ( H `  ( N `  suc  k ) ) -1-1-onto-> ( F " suc  k
)  <->  ( ( H `
 ( N `  suc  k ) ) : dom  ( H `  ( N `  suc  k
) ) -1-1-> ( F
" suc  k )  /\  ran  ( H `  ( N `  suc  k
) )  =  ( F " suc  k
) ) )
102100, 101sylib 121 . . . . . . . . . . 11  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( ( H `  ( N `  suc  k
) ) : dom  ( H `  ( N `
 suc  k )
) -1-1-> ( F " suc  k )  /\  ran  ( H `  ( N `
 suc  k )
)  =  ( F
" suc  k )
) )
103102simprd 113 . . . . . . . . . 10  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  ran  ( H `  ( N `  suc  k ) )  =  ( F
" suc  k )
)
104103adantr 274 . . . . . . . . 9  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  ->  ran  ( H `  ( N `  suc  k ) )  =  ( F
" suc  k )
)
10590, 94, 1043eqtr3d 2211 . . . . . . . 8  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  -> 
( F " ( `' N `  P ) )  =  ( F
" suc  k )
)
10633, 105eleqtrrd 2250 . . . . . . 7  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  -> 
( F `  k
)  e.  ( F
" ( `' N `  P ) ) )
107 fvelima 5548 . . . . . . 7  |-  ( ( Fun  F  /\  ( F `  k )  e.  ( F " ( `' N `  P ) ) )  ->  E. q  e.  ( `' N `  P ) ( F `
 q )  =  ( F `  k
) )
10822, 106, 107syl2anc 409 . . . . . 6  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  ->  E. q  e.  ( `' N `  P ) ( F `  q
)  =  ( F `
 k ) )
109 simprr 527 . . . . . . 7  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  ( q  e.  ( `' N `  P )  /\  ( F `  q )  =  ( F `  k ) ) )  ->  ( F `  q )  =  ( F `  k ) )
110 fveq2 5496 . . . . . . . . . 10  |-  ( j  =  q  ->  ( F `  j )  =  ( F `  q ) )
111110neeq2d 2359 . . . . . . . . 9  |-  ( j  =  q  ->  (
( F `  k
)  =/=  ( F `
 j )  <->  ( F `  k )  =/=  ( F `  q )
) )
11267ad2antrr 485 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  ( q  e.  ( `' N `  P )  /\  ( F `  q )  =  ( F `  k ) ) )  ->  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) )
113 elelsuc 4394 . . . . . . . . . 10  |-  ( q  e.  ( `' N `  P )  ->  q  e.  suc  ( `' N `  P ) )
114113ad2antrl 487 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  ( q  e.  ( `' N `  P )  /\  ( F `  q )  =  ( F `  k ) ) )  ->  q  e.  suc  ( `' N `  P ) )
115111, 112, 114rspcdva 2839 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  ( q  e.  ( `' N `  P )  /\  ( F `  q )  =  ( F `  k ) ) )  ->  ( F `  k )  =/=  ( F `  q
) )
116115necomd 2426 . . . . . . 7  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  ( q  e.  ( `' N `  P )  /\  ( F `  q )  =  ( F `  k ) ) )  ->  ( F `  q )  =/=  ( F `  k
) )
117109, 116pm2.21ddne 2423 . . . . . 6  |-  ( ( ( ( ph  /\  ( k  e.  om  /\ 
A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  /\  ( q  e.  ( `' N `  P )  /\  ( F `  q )  =  ( F `  k ) ) )  -> F.  )
118108, 117rexlimddv 2592 . . . . 5  |-  ( ( ( ph  /\  (
k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )  /\  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) ) )  -> F.  )
119118inegd 1367 . . . 4  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  -.  dom  ( H `  P )  =  dom  ( H `  ( N `
 suc  k )
) )
120 dmss 4810 . . . . . 6  |-  ( ( H `  P ) 
C_  ( H `  ( N `  suc  k
) )  ->  dom  ( H `  P ) 
C_  dom  ( H `  ( N `  suc  k ) ) )
12176, 120syl 14 . . . . 5  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  dom  ( H `  P
)  C_  dom  ( H `
 ( N `  suc  k ) ) )
12235, 19, 4, 50, 5, 51, 52, 11ennnfonelemom 12363 . . . . . . 7  |-  ( ph  ->  dom  ( H `  P )  e.  om )
123122adantr 274 . . . . . 6  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  dom  ( H `  P
)  e.  om )
12442a1i 9 . . . . . . . . 9  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( E. k  e. 
om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  E. k  e.  om  A. a  e.  suc  n ( F `  k )  =/=  ( F `  a ) ) )
125124ralbidv 2470 . . . . . . . 8  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( A. n  e. 
om  E. k  e.  om  A. j  e.  suc  n
( F `  k
)  =/=  ( F `
 j )  <->  A. n  e.  om  E. k  e. 
om  A. a  e.  suc  n ( F `  k )  =/=  ( F `  a )
) )
12638, 125mpbid 146 . . . . . . 7  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  A. n  e.  om  E. k  e.  om  A. a  e.  suc  n ( F `  k )  =/=  ( F `  a ) )
12736, 37, 126, 50, 5, 51, 52, 61ennnfonelemom 12363 . . . . . 6  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  dom  ( H `  ( N `  suc  k ) )  e.  om )
128 nntri1 6475 . . . . . 6  |-  ( ( dom  ( H `  P )  e.  om  /\ 
dom  ( H `  ( N `  suc  k
) )  e.  om )  ->  ( dom  ( H `  P )  C_ 
dom  ( H `  ( N `  suc  k
) )  <->  -.  dom  ( H `  ( N `  suc  k ) )  e.  dom  ( H `
 P ) ) )
129123, 127, 128syl2anc 409 . . . . 5  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( dom  ( H `  P )  C_  dom  ( H `  ( N `
 suc  k )
)  <->  -.  dom  ( H `
 ( N `  suc  k ) )  e. 
dom  ( H `  P ) ) )
130121, 129mpbid 146 . . . 4  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  -.  dom  ( H `  ( N `  suc  k
) )  e.  dom  ( H `  P ) )
131 nntri3or 6472 . . . . 5  |-  ( ( dom  ( H `  P )  e.  om  /\ 
dom  ( H `  ( N `  suc  k
) )  e.  om )  ->  ( dom  ( H `  P )  e.  dom  ( H `  ( N `  suc  k
) )  \/  dom  ( H `  P )  =  dom  ( H `
 ( N `  suc  k ) )  \/ 
dom  ( H `  ( N `  suc  k
) )  e.  dom  ( H `  P ) ) )
132123, 127, 131syl2anc 409 . . . 4  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( dom  ( H `  P )  e.  dom  ( H `  ( N `
 suc  k )
)  \/  dom  ( H `  P )  =  dom  ( H `  ( N `  suc  k
) )  \/  dom  ( H `  ( N `
 suc  k )
)  e.  dom  ( H `  P )
) )
133119, 130, 132ecase23d 1345 . . 3  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  dom  ( H `  P
)  e.  dom  ( H `  ( N `  suc  k ) ) )
134 fveq2 5496 . . . . . 6  |-  ( i  =  ( N `  suc  k )  ->  ( H `  i )  =  ( H `  ( N `  suc  k
) ) )
135134dmeqd 4813 . . . . 5  |-  ( i  =  ( N `  suc  k )  ->  dom  ( H `  i )  =  dom  ( H `
 ( N `  suc  k ) ) )
136135eleq2d 2240 . . . 4  |-  ( i  =  ( N `  suc  k )  ->  ( dom  ( H `  P
)  e.  dom  ( H `  i )  <->  dom  ( H `  P
)  e.  dom  ( H `  ( N `  suc  k ) ) ) )
137136rspcev 2834 . . 3  |-  ( ( ( N `  suc  k )  e.  NN0  /\ 
dom  ( H `  P )  e.  dom  ( H `  ( N `
 suc  k )
) )  ->  E. i  e.  NN0  dom  ( H `  P )  e.  dom  ( H `  i ) )
13818, 133, 137syl2anc 409 . 2  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  E. i  e.  NN0  dom  ( H `  P
)  e.  dom  ( H `  i )
)
13913, 138rexlimddv 2592 1  |-  ( ph  ->  E. i  e.  NN0  dom  ( H `  P
)  e.  dom  ( H `  i )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104  DECID wdc 829    \/ w3o 972    = wceq 1348   F. wfal 1353    e. wcel 2141    =/= wne 2340   A.wral 2448   E.wrex 2449    u. cun 3119    C_ wss 3121   (/)c0 3414   ifcif 3526   {csn 3583   <.cop 3586   class class class wbr 3989    |-> cmpt 4050   suc csuc 4350   omcom 4574   `'ccnv 4610   dom cdm 4611   ran crn 4612   "cima 4614   Fun wfun 5192   -->wf 5194   -1-1->wf1 5195   -onto->wfo 5196   -1-1-onto->wf1o 5197   ` cfv 5198  (class class class)co 5853    e. cmpo 5855  freccfrec 6369    ^pm cpm 6627   0cc0 7774   1c1 7775    + caddc 7777    < clt 7954    - cmin 8090   NN0cn0 9135   ZZcz 9212    seqcseq 10401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-addcom 7874  ax-addass 7876  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-0id 7882  ax-rnegex 7883  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-ltadd 7890
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-iord 4351  df-on 4353  df-ilim 4354  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-frec 6370  df-pm 6629  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-inn 8879  df-n0 9136  df-z 9213  df-uz 9488  df-seqfrec 10402
This theorem is referenced by:  ennnfonelemhom  12370
  Copyright terms: Public domain W3C validator