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

Theorem ennnfonelemex 12239
Description: Lemma for ennnfone 12250. 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 4365 . . . . 5  |-  ( n  =  ( `' N `  P )  ->  suc  n  =  suc  ( `' N `  P ) )
21raleqdv 2658 . . . 4  |-  ( n  =  ( `' N `  P )  ->  ( A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) ) )
32rexbidv 2458 . . 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 10337 . . . . . 6  |-  N : om
-1-1-onto-> NN0
7 f1ocnv 5430 . . . . . 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 5417 . . . . 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 5606 . . 3  |-  ( ph  ->  ( `' N `  P )  e.  om )
133, 4, 12rspcdva 2821 . 2  |-  ( ph  ->  E. k  e.  om  A. j  e.  suc  ( `' N `  P ) ( F `  k
)  =/=  ( F `
 j ) )
14 f1of 5417 . . . . 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 4557 . . . . 5  |-  ( k  e.  om  ->  suc  k  e.  om )
1716ad2antrl 482 . . . 4  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  suc  k  e.  om )
1815, 17ffvelrnd 5606 . . 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 480 . . . . . . . 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 5396 . . . . . . . 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 2715 . . . . . . . . . 10  |-  k  e. 
_V
2423sucid 4380 . . . . . . . . 9  |-  k  e. 
suc  k
25 simprl 521 . . . . . . . . . . . 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 5395 . . . . . . . . . . . 12  |-  ( F : om -onto-> A  ->  F : om --> A )
28 fdm 5328 . . . . . . . . . . . 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 2237 . . . . . . . . . 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 5701 . . . . . . . . . 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 5471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  a  ->  ( F `  j )  =  ( F `  a ) )
4039neeq2d 2346 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  a  ->  (
( F `  k
)  =/=  ( F `
 j )  <->  ( F `  k )  =/=  ( F `  a )
) )
4140cbvralv 2680 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  A. a  e.  suc  n ( F `
 k )  =/=  ( F `  a
) )
4241rexbii 2464 . . . . . . . . . . . . . . . . . . . 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 5471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  b  ->  ( F `  k )  =  ( F `  b ) )
4443neeq1d 2345 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  b  ->  (
( F `  k
)  =/=  ( F `
 a )  <->  ( F `  b )  =/=  ( F `  a )
) )
4544ralbidv 2457 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  b  ->  ( A. a  e.  suc  n ( F `  k )  =/=  ( F `  a )  <->  A. a  e.  suc  n
( F `  b
)  =/=  ( F `
 a ) ) )
4645cbvrexv 2681 . . . . . . . . . . . . . . . . . . . 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 2463 . . . . . . . . . . . . . . . . . 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 12238 . . . . . . . . . . . . . . . 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 5419 . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . 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 5606 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  om )  ->  ( N `  suc  k )  e. 
NN0 )
6160adantrr 471 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  suc  k )  e.  NN0 )
6257nn0red 9150 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  P  e.  RR )
6361nn0red 9150 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( N `  suc  k )  e.  RR )
64 f1ocnvfv2 5731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N : om -1-1-onto-> NN0  /\  P  e. 
NN0 )  ->  ( N `  ( `' N `  P )
)  =  P )
656, 57, 64sylancr 411 . . . . . . . . . . . . . . . . . 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 522 . . . . . . . . . . . . . . . . . . . . 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 12225 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( `' N `  P )  e.  k )
69 elelsuc 4372 . . . . . . . . . . . . . . . . . . . 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 9185 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
0  e.  ZZ )
7271, 5, 66, 17frec2uzltd 10312 . . . . . . . . . . . . . . . . . . 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 3991 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  P  <  ( N `  suc  k ) )
7562, 63, 74ltled 7999 . . . . . . . . . . . . . . . 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 12236 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( H `  P
)  C_  ( H `  ( N `  suc  k ) ) )
7776ad2antrr 480 . . . . . . . . . . . . . 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 5497 . . . . . . . . . . . . . 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 1220 . . . . . . . . . . . . 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 2163 . . . . . . . . . . . 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 2530 . . . . . . . . . . 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 12238 . . . . . . . . . . . . . 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 5419 . . . . . . . . . . . . . 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 5573 . . . . . . . . . . . . 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 929 . . . . . . . . . 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 4818 . . . . . . . . 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 5426 . . . . . . . . . . . 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 5730 . . . . . . . . . . . . . . . 16  |-  ( ( N : om -1-1-onto-> NN0  /\  suc  k  e.  om )  ->  ( `' N `  ( N `
 suc  k )
)  =  suc  k
)
966, 17, 95sylancr 411 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  -> 
( `' N `  ( N `  suc  k
) )  =  suc  k )
9796imaeq2d 4931 . . . . . . . . . . . . . 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 5408 . . . . . . . . . . . . . 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 5426 . . . . . . . . . . . 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 2198 . . . . . . . 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 2237 . . . . . . 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 5523 . . . . . . 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 522 . . . . . . 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 5471 . . . . . . . . . 10  |-  ( j  =  q  ->  ( F `  j )  =  ( F `  q ) )
111110neeq2d 2346 . . . . . . . . 9  |-  ( j  =  q  ->  (
( F `  k
)  =/=  ( F `
 j )  <->  ( F `  k )  =/=  ( F `  q )
) )
11267ad2antrr 480 . . . . . . . . 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 4372 . . . . . . . . . 10  |-  ( q  e.  ( `' N `  P )  ->  q  e.  suc  ( `' N `  P ) )
114113ad2antrl 482 . . . . . . . . 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 2821 . . . . . . . 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 2413 . . . . . . 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 2410 . . . . . 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 2579 . . . . 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 1354 . . . 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 4788 . . . . . 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 12233 . . . . . . 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 2457 . . . . . . . 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 12233 . . . . . 6  |-  ( (
ph  /\  ( k  e.  om  /\  A. j  e.  suc  ( `' N `  P ) ( F `
 k )  =/=  ( F `  j
) ) )  ->  dom  ( H `  ( N `  suc  k ) )  e.  om )
128 nntri1 6446 . . . . . 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 6443 . . . . 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 1332 . . 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 5471 . . . . . 6  |-  ( i  =  ( N `  suc  k )  ->  ( H `  i )  =  ( H `  ( N `  suc  k
) ) )
135134dmeqd 4791 . . . . 5  |-  ( i  =  ( N `  suc  k )  ->  dom  ( H `  i )  =  dom  ( H `
 ( N `  suc  k ) ) )
136135eleq2d 2227 . . . 4  |-  ( i  =  ( N `  suc  k )  ->  ( dom  ( H `  P
)  e.  dom  ( H `  i )  <->  dom  ( H `  P
)  e.  dom  ( H `  ( N `  suc  k ) ) ) )
137136rspcev 2816 . . 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 2579 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 820    \/ w3o 962    = wceq 1335   F. wfal 1340    e. wcel 2128    =/= wne 2327   A.wral 2435   E.wrex 2436    u. cun 3100    C_ wss 3102   (/)c0 3395   ifcif 3506   {csn 3561   <.cop 3564   class class class wbr 3967    |-> cmpt 4028   suc csuc 4328   omcom 4552   `'ccnv 4588   dom cdm 4589   ran crn 4590   "cima 4592   Fun wfun 5167   -->wf 5169   -1-1->wf1 5170   -onto->wfo 5171   -1-1-onto->wf1o 5172   ` cfv 5173  (class class class)co 5827    e. cmpo 5829  freccfrec 6340    ^pm cpm 6597   0cc0 7735   1c1 7736    + caddc 7738    < clt 7915    - cmin 8051   NN0cn0 9096   ZZcz 9173    seqcseq 10354
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 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4082  ax-sep 4085  ax-nul 4093  ax-pow 4138  ax-pr 4172  ax-un 4396  ax-setind 4499  ax-iinf 4550  ax-cnex 7826  ax-resscn 7827  ax-1cn 7828  ax-1re 7829  ax-icn 7830  ax-addcl 7831  ax-addrcl 7832  ax-mulcl 7833  ax-addcom 7835  ax-addass 7837  ax-distr 7839  ax-i2m1 7840  ax-0lt1 7841  ax-0id 7843  ax-rnegex 7844  ax-cnre 7846  ax-pre-ltirr 7847  ax-pre-ltwlin 7848  ax-pre-lttrn 7849  ax-pre-ltadd 7851
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3396  df-if 3507  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-uni 3775  df-int 3810  df-iun 3853  df-br 3968  df-opab 4029  df-mpt 4030  df-tr 4066  df-id 4256  df-iord 4329  df-on 4331  df-ilim 4332  df-suc 4334  df-iom 4553  df-xp 4595  df-rel 4596  df-cnv 4597  df-co 4598  df-dm 4599  df-rn 4600  df-res 4601  df-ima 4602  df-iota 5138  df-fun 5175  df-fn 5176  df-f 5177  df-f1 5178  df-fo 5179  df-f1o 5180  df-fv 5181  df-riota 5783  df-ov 5830  df-oprab 5831  df-mpo 5832  df-1st 6091  df-2nd 6092  df-recs 6255  df-frec 6341  df-pm 6599  df-pnf 7917  df-mnf 7918  df-xr 7919  df-ltxr 7920  df-le 7921  df-sub 8053  df-neg 8054  df-inn 8840  df-n0 9097  df-z 9174  df-uz 9446  df-seqfrec 10355
This theorem is referenced by:  ennnfonelemhom  12240
  Copyright terms: Public domain W3C validator