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

Theorem ennnfonelemex 11822
Description: Lemma for ennnfone 11833. 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 4292 . . . . 5  |-  ( n  =  ( `' N `  P )  ->  suc  n  =  suc  ( `' N `  P ) )
21raleqdv 2607 . . . 4  |-  ( n  =  ( `' N `  P )  ->  ( A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )
32rexbidv 2413 . . 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 10141 . . . . . 6  |-  N : om
-1-1-onto-> NN0
7 f1ocnv 5346 . . . . . 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 5333 . . . . 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 5522 . . 3  |-  ( ph  ->  ( `' N `  P )  e.  om )
133, 4, 12rspcdva 2766 . 2  |-  ( ph  ->  E. k  e.  om  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) )
14 f1of 5333 . . . . 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 4477 . . . . 5  |-  ( k  e.  om  ->  suc  k  e.  om )
1716ad2antrl 479 . . . 4  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  suc  k  e.  om )
1815, 17ffvelrnd 5522 . . 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 477 . . . . . . . 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 5314 . . . . . . . 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 2661 . . . . . . . . . 10  |-  k  e. 
_V
2423sucid 4307 . . . . . . . . 9  |-  k  e. 
suc  k
25 simprl 503 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
k  e.  om )
2625adantr 272 . . . . . . . . . . 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 5313 . . . . . . . . . . . 12  |-  ( F : om -onto-> A  ->  F : om --> A )
28 fdm 5246 . . . . . . . . . . . 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 2195 . . . . . . . . . 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 5615 . . . . . . . . . 10  |-  ( ( Fun  F  /\  k  e.  dom  F )  -> 
( k  e.  suc  k  ->  ( F `  k )  e.  ( F " suc  k
) ) )
3222, 30, 31syl2anc 406 . . . . . . . . 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 272 . . . . . . . . . . . . . . . . 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 272 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  F : om -onto-> A )
384adantr 272 . . . . . . . . . . . . . . . . . 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 5387 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  a  ->  ( F `  j )  =  ( F `  a ) )
4039neeq2d 2302 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  a  ->  (
( F `  k
)  =/=  ( F `
 j )  <->  ( F `  k )  =/=  ( F `  a )
) )
4140cbvralv 2629 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  A. a  e.  suc  n ( F `
 k )  =/=  ( F `  a
) )
4241rexbii 2417 . . . . . . . . . . . . . . . . . . . 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 5387 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  b  ->  ( F `  k )  =  ( F `  b ) )
4443neeq1d 2301 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  b  ->  (
( F `  k
)  =/=  ( F `
 a )  <->  ( F `  b )  =/=  ( F `  a )
) )
4544ralbidv 2412 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  b  ->  ( A. a  e.  suc  n ( F `  k )  =/=  ( F `  a )  <->  A. a  e.  suc  n
( F `  b
)  =/=  ( F `
 a ) ) )
4645cbvrexv 2630 . . . . . . . . . . . . . . . . . . . 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 2416 . . . . . . . . . . . . . . . . . 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 11821 . . . . . . . . . . . . . . . 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 5335 . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . 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 272 . . . . . . . . . . . . . . . 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 273 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  om )  ->  suc  k  e. 
om )
6058, 59ffvelrnd 5522 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  om )  ->  ( N `  suc  k )  e. 
NN0 )
6160adantrr 468 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  suc  k )  e.  NN0 )
6257nn0red 8982 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  P  e.  RR )
6361nn0red 8982 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  suc  k )  e.  RR )
64 f1ocnvfv2 5645 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N : om -1-1-onto-> NN0  /\  P  e. 
NN0 )  ->  ( N `  ( `' N `  P )
)  =  P )
656, 57, 64sylancr 408 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  ( `' N `  P ) )  =  P )
6612adantr 272 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( `' N `  P )  e.  om )
67 simprr 504 . . . . . . . . . . . . . . . . . . . . 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 11808 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( `' N `  P )  e.  k )
69 elelsuc 4299 . . . . . . . . . . . . . . . . . . . 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 9017 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
0  e.  ZZ )
7271, 5, 66, 17frec2uzltd 10116 . . . . . . . . . . . . . . . . . . 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 3920 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  P  <  ( N `  suc  k ) )
7562, 63, 74ltled 7845 . . . . . . . . . . . . . . . 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 11819 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( H `  P
)  C_  ( H `  ( N `  suc  k ) ) )
7776ad2antrr 477 . . . . . . . . . . . . . 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 5413 . . . . . . . . . . . . . 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 1199 . . . . . . . . . . . . 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 2121 . . . . . . . . . . . 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 2480 . . . . . . . . . . 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 11821 . . . . . . . . . . . . . 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 5335 . . . . . . . . . . . . . 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 5489 . . . . . . . . . . . . 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 406 . . . . . . . . . . . 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 272 . . . . . . . . . . 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 911 . . . . . . . . . 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 4736 . . . . . . . . 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 5342 . . . . . . . . . . . 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 272 . . . . . . . . 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 5644 . . . . . . . . . . . . . . . 16  |-  ( ( N : om -1-1-onto-> NN0  /\  suc  k  e.  om )  ->  ( `' N `  ( N `
 suc  k )
)  =  suc  k
)
966, 17, 95sylancr 408 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( `' N `  ( N `  suc  k
) )  =  suc  k )
9796imaeq2d 4849 . . . . . . . . . . . . . 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 5326 . . . . . . . . . . . . . 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 5342 . . . . . . . . . . . 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 272 . . . . . . . . 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 2156 . . . . . . . 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 2195 . . . . . . 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 5439 . . . . . . 7  |-  ( ( Fun  F  /\  ( F `  k )  e.  ( F " ( `' N `  P ) ) )  ->  E. q  e.  ( `' N `  P ) ( F `
 q )  =  ( F `  k
) )
10822, 106, 107syl2anc 406 . . . . . 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 504 . . . . . . 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 5387 . . . . . . . . . 10  |-  ( j  =  q  ->  ( F `  j )  =  ( F `  q ) )
111110neeq2d 2302 . . . . . . . . 9  |-  ( j  =  q  ->  (
( F `  k
)  =/=  ( F `
 j )  <->  ( F `  k )  =/=  ( F `  q )
) )
11267ad2antrr 477 . . . . . . . . 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 4299 . . . . . . . . . 10  |-  ( q  e.  ( `' N `  P )  ->  q  e.  suc  ( `' N `  P ) )
114113ad2antrl 479 . . . . . . . . 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 2766 . . . . . . . 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 2369 . . . . . . 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 2366 . . . . . 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 2529 . . . . 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 1333 . . . 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 4706 . . . . . 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 11816 . . . . . . 7  |-  ( ph  ->  dom  ( H `  P )  e.  om )
123122adantr 272 . . . . . 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 2412 . . . . . . . 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 11816 . . . . . 6  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  dom  ( H `  ( N `  suc  k ) )  e.  om )
128 nntri1 6358 . . . . . 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 406 . . . . 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 6355 . . . . 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 406 . . . 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 1311 . . 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 5387 . . . . . 6  |-  ( i  =  ( N `  suc  k )  ->  ( H `  i )  =  ( H `  ( N `  suc  k
) ) )
135134dmeqd 4709 . . . . 5  |-  ( i  =  ( N `  suc  k )  ->  dom  ( H `  i )  =  dom  ( H `
 ( N `  suc  k ) ) )
136135eleq2d 2185 . . . 4  |-  ( i  =  ( N `  suc  k )  ->  ( dom  ( H `  P
)  e.  dom  ( H `  i )  <->  dom  ( H `  P
)  e.  dom  ( H `  ( N `  suc  k ) ) ) )
137136rspcev 2761 . . 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 406 . 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 2529 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 802    \/ w3o 944    = wceq 1314   F. wfal 1319    e. wcel 1463    =/= wne 2283   A.wral 2391   E.wrex 2392    u. cun 3037    C_ wss 3039   (/)c0 3331   ifcif 3442   {csn 3495   <.cop 3498   class class class wbr 3897    |-> cmpt 3957   suc csuc 4255   omcom 4472   `'ccnv 4506   dom cdm 4507   ran crn 4508   "cima 4510   Fun wfun 5085   -->wf 5087   -1-1->wf1 5088   -onto->wfo 5089   -1-1-onto->wf1o 5090   ` cfv 5091  (class class class)co 5740    e. cmpo 5742  freccfrec 6253    ^pm cpm 6509   0cc0 7584   1c1 7585    + caddc 7587    < clt 7764    - cmin 7897   NN0cn0 8928   ZZcz 9005    seqcseq 10158
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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-addcom 7684  ax-addass 7686  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-0id 7692  ax-rnegex 7693  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-ltadd 7700
This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-frec 6254  df-pm 6511  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-inn 8678  df-n0 8929  df-z 9006  df-uz 9276  df-seqfrec 10159
This theorem is referenced by:  ennnfonelemhom  11823
  Copyright terms: Public domain W3C validator