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

Theorem ennnfonelemhom 12469
Description: Lemma for ennnfone 12479. The sequences in  H increase in length without bound if you go out far enough. (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 )
ennnfonelemhom.m  |-  ( ph  ->  M  e.  om )
Assertion
Ref Expression
ennnfonelemhom  |-  ( ph  ->  E. i  e.  NN0  M  e.  dom  ( H `
 i ) )
Distinct variable groups:    i, H, k, j, x, y    i, M    ph, i, k, x, y, j    ph, n    x, N, y, j, k   
n, N    j, G    k, F, x, y, j   
n, F, j    x, A, y, j    j, J   
x, i, y, j   
i, n, H, k
Allowed substitution hints:    A( i, k, n)    F( i)    G( x, y, i, k, n)    J( x, y, i, k, n)    M( x, y, j, k, n)    N( i)

Proof of Theorem ennnfonelemhom
Dummy variables  q  w  a are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ennnfonelemhom.m . 2  |-  ( ph  ->  M  e.  om )
2 eleq1 2252 . . . . 5  |-  ( w  =  (/)  ->  ( w  e.  dom  ( H `
 i )  <->  (/)  e.  dom  ( H `  i ) ) )
32rexbidv 2491 . . . 4  |-  ( w  =  (/)  ->  ( E. i  e.  NN0  w  e.  dom  ( H `  i )  <->  E. i  e.  NN0  (/)  e.  dom  ( H `  i )
) )
43imbi2d 230 . . 3  |-  ( w  =  (/)  ->  ( (
ph  ->  E. i  e.  NN0  w  e.  dom  ( H `
 i ) )  <-> 
( ph  ->  E. i  e.  NN0  (/)  e.  dom  ( H `  i )
) ) )
5 eleq1 2252 . . . . 5  |-  ( w  =  k  ->  (
w  e.  dom  ( H `  i )  <->  k  e.  dom  ( H `
 i ) ) )
65rexbidv 2491 . . . 4  |-  ( w  =  k  ->  ( E. i  e.  NN0  w  e.  dom  ( H `
 i )  <->  E. i  e.  NN0  k  e.  dom  ( H `  i ) ) )
76imbi2d 230 . . 3  |-  ( w  =  k  ->  (
( ph  ->  E. i  e.  NN0  w  e.  dom  ( H `  i ) )  <->  ( ph  ->  E. i  e.  NN0  k  e.  dom  ( H `  i ) ) ) )
8 eleq1 2252 . . . . 5  |-  ( w  =  suc  k  -> 
( w  e.  dom  ( H `  i )  <->  suc  k  e.  dom  ( H `  i ) ) )
98rexbidv 2491 . . . 4  |-  ( w  =  suc  k  -> 
( E. i  e. 
NN0  w  e.  dom  ( H `  i )  <->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i )
) )
109imbi2d 230 . . 3  |-  ( w  =  suc  k  -> 
( ( ph  ->  E. i  e.  NN0  w  e.  dom  ( H `  i ) )  <->  ( ph  ->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i )
) ) )
11 eleq1 2252 . . . . 5  |-  ( w  =  M  ->  (
w  e.  dom  ( H `  i )  <->  M  e.  dom  ( H `
 i ) ) )
1211rexbidv 2491 . . . 4  |-  ( w  =  M  ->  ( E. i  e.  NN0  w  e.  dom  ( H `
 i )  <->  E. i  e.  NN0  M  e.  dom  ( H `  i ) ) )
1312imbi2d 230 . . 3  |-  ( w  =  M  ->  (
( ph  ->  E. i  e.  NN0  w  e.  dom  ( H `  i ) )  <->  ( ph  ->  E. i  e.  NN0  M  e.  dom  ( H `  i ) ) ) )
14 1nn0 9223 . . . 4  |-  1  e.  NN0
15 0ex 4145 . . . . . 6  |-  (/)  e.  _V
1615snid 3638 . . . . 5  |-  (/)  e.  { (/)
}
17 ennnfonelemh.dceq . . . . . . . 8  |-  ( ph  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y )
18 ennnfonelemh.f . . . . . . . 8  |-  ( ph  ->  F : om -onto-> A
)
19 ennnfonelemh.ne . . . . . . . 8  |-  ( ph  ->  A. n  e.  om  E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j ) )
20 ennnfonelemh.g . . . . . . . 8  |-  G  =  ( x  e.  ( A  ^pm  om ) ,  y  e.  om  |->  if ( ( F `  y )  e.  ( F " y ) ,  x ,  ( x  u.  { <. dom  x ,  ( F `
 y ) >. } ) ) )
21 ennnfonelemh.n . . . . . . . 8  |-  N  = frec ( ( x  e.  ZZ  |->  ( x  + 
1 ) ) ,  0 )
22 ennnfonelemh.j . . . . . . . 8  |-  J  =  ( x  e.  NN0  |->  if ( x  =  0 ,  (/) ,  ( `' N `  ( x  -  1 ) ) ) )
23 ennnfonelemh.h . . . . . . . 8  |-  H  =  seq 0 ( G ,  J )
2417, 18, 19, 20, 21, 22, 23ennnfonelem1 12461 . . . . . . 7  |-  ( ph  ->  ( H `  1
)  =  { <. (/)
,  ( F `  (/) ) >. } )
2524dmeqd 4847 . . . . . 6  |-  ( ph  ->  dom  ( H ` 
1 )  =  dom  {
<. (/) ,  ( F `
 (/) ) >. } )
26 peano1 4611 . . . . . . . 8  |-  (/)  e.  om
27 fof 5457 . . . . . . . . . 10  |-  ( F : om -onto-> A  ->  F : om --> A )
2818, 27syl 14 . . . . . . . . 9  |-  ( ph  ->  F : om --> A )
2926a1i 9 . . . . . . . . 9  |-  ( ph  -> 
(/)  e.  om )
3028, 29ffvelcdmd 5673 . . . . . . . 8  |-  ( ph  ->  ( F `  (/) )  e.  A )
31 fnsng 5282 . . . . . . . 8  |-  ( (
(/)  e.  om  /\  ( F `  (/) )  e.  A )  ->  { <. (/)
,  ( F `  (/) ) >. }  Fn  { (/)
} )
3226, 30, 31sylancr 414 . . . . . . 7  |-  ( ph  ->  { <. (/) ,  ( F `
 (/) ) >. }  Fn  {
(/) } )
33 fndm 5334 . . . . . . 7  |-  ( {
<. (/) ,  ( F `
 (/) ) >. }  Fn  {
(/) }  ->  dom  { <.
(/) ,  ( F `  (/) ) >. }  =  { (/) } )
3432, 33syl 14 . . . . . 6  |-  ( ph  ->  dom  { <. (/) ,  ( F `  (/) ) >. }  =  { (/) } )
3525, 34eqtrd 2222 . . . . 5  |-  ( ph  ->  dom  ( H ` 
1 )  =  { (/)
} )
3616, 35eleqtrrid 2279 . . . 4  |-  ( ph  -> 
(/)  e.  dom  ( H `
 1 ) )
37 fveq2 5534 . . . . . . 7  |-  ( i  =  1  ->  ( H `  i )  =  ( H ` 
1 ) )
3837dmeqd 4847 . . . . . 6  |-  ( i  =  1  ->  dom  ( H `  i )  =  dom  ( H `
 1 ) )
3938eleq2d 2259 . . . . 5  |-  ( i  =  1  ->  ( (/) 
e.  dom  ( H `  i )  <->  (/)  e.  dom  ( H `  1 ) ) )
4039rspcev 2856 . . . 4  |-  ( ( 1  e.  NN0  /\  (/) 
e.  dom  ( H `  1 ) )  ->  E. i  e.  NN0  (/) 
e.  dom  ( H `  i ) )
4114, 36, 40sylancr 414 . . 3  |-  ( ph  ->  E. i  e.  NN0  (/) 
e.  dom  ( H `  i ) )
4217ad3antrrr 492 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y
)
4318ad3antrrr 492 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  F : om -onto-> A )
4419ad3antrrr 492 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  A. n  e.  om  E. k  e. 
om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )
)
45 fveq2 5534 . . . . . . . . . . . . . 14  |-  ( k  =  a  ->  ( F `  k )  =  ( F `  a ) )
4645neeq1d 2378 . . . . . . . . . . . . 13  |-  ( k  =  a  ->  (
( F `  k
)  =/=  ( F `
 j )  <->  ( F `  a )  =/=  ( F `  j )
) )
4746ralbidv 2490 . . . . . . . . . . . 12  |-  ( k  =  a  ->  ( A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  A. j  e.  suc  n
( F `  a
)  =/=  ( F `
 j ) ) )
4847cbvrexv 2719 . . . . . . . . . . 11  |-  ( E. k  e.  om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )  <->  E. a  e.  om  A. j  e. 
suc  n ( F `
 a )  =/=  ( F `  j
) )
4948ralbii 2496 . . . . . . . . . 10  |-  ( A. n  e.  om  E. k  e.  om  A. j  e. 
suc  n ( F `
 k )  =/=  ( F `  j
)  <->  A. n  e.  om  E. a  e.  om  A. j  e.  suc  n ( F `  a )  =/=  ( F `  j ) )
5044, 49sylib 122 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  A. n  e.  om  E. a  e. 
om  A. j  e.  suc  n ( F `  a )  =/=  ( F `  j )
)
51 simplr 528 . . . . . . . . 9  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  i  e.  NN0 )
5242, 43, 50, 20, 21, 22, 23, 51ennnfonelemex 12468 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  E. q  e.  NN0  dom  ( H `  i )  e.  dom  ( H `  q ) )
5342ad2antrr 488 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  A. x  e.  A  A. y  e.  A DECID  x  =  y
)
5443ad2antrr 488 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  F : om -onto-> A )
5544ad2antrr 488 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  A. n  e.  om  E. k  e. 
om  A. j  e.  suc  n ( F `  k )  =/=  ( F `  j )
)
56 simplr 528 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  q  e.  NN0 )
5753, 54, 55, 20, 21, 22, 23, 56ennnfonelemom 12462 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  dom  ( H `
 q )  e. 
om )
58 nnord 4629 . . . . . . . . . . . . 13  |-  ( dom  ( H `  q
)  e.  om  ->  Ord 
dom  ( H `  q ) )
5957, 58syl 14 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  Ord  dom  ( H `  q )
)
60 simpr 110 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  dom  ( H `
 i )  e. 
dom  ( H `  q ) )
61 ordsucss 4521 . . . . . . . . . . . 12  |-  ( Ord 
dom  ( H `  q )  ->  ( dom  ( H `  i
)  e.  dom  ( H `  q )  ->  suc  dom  ( H `  i )  C_  dom  ( H `  q ) ) )
6259, 60, 61sylc 62 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  suc  dom  ( H `  i )  C_ 
dom  ( H `  q ) )
63 simpr 110 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  k  e.  dom  ( H `  i
) )
6442, 43, 44, 20, 21, 22, 23, 51ennnfonelemom 12462 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  dom  ( H `
 i )  e. 
om )
65 nnsucelsuc 6517 . . . . . . . . . . . . . 14  |-  ( dom  ( H `  i
)  e.  om  ->  ( k  e.  dom  ( H `  i )  <->  suc  k  e.  suc  dom  ( H `  i ) ) )
6664, 65syl 14 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  ( k  e.  dom  ( H `  i )  <->  suc  k  e. 
suc  dom  ( H `  i ) ) )
6763, 66mpbid 147 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  suc  k  e. 
suc  dom  ( H `  i ) )
6867ad2antrr 488 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  suc  k  e. 
suc  dom  ( H `  i ) )
6962, 68sseldd 3171 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  k  e.  om )  /\  i  e. 
NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e.  NN0 )  /\  dom  ( H `  i
)  e.  dom  ( H `  q )
)  ->  suc  k  e. 
dom  ( H `  q ) )
7069ex 115 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  /\  q  e. 
NN0 )  ->  ( dom  ( H `  i
)  e.  dom  ( H `  q )  ->  suc  k  e.  dom  ( H `  q ) ) )
7170reximdva 2592 . . . . . . . 8  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  ( E. q  e.  NN0  dom  ( H `  i )  e.  dom  ( H `  q )  ->  E. q  e.  NN0  suc  k  e.  dom  ( H `  q
) ) )
7252, 71mpd 13 . . . . . . 7  |-  ( ( ( ( ph  /\  k  e.  om )  /\  i  e.  NN0 )  /\  k  e.  dom  ( H `  i ) )  ->  E. q  e.  NN0  suc  k  e.  dom  ( H `  q
) )
7372rexlimdva2 2610 . . . . . 6  |-  ( (
ph  /\  k  e.  om )  ->  ( E. i  e.  NN0  k  e. 
dom  ( H `  i )  ->  E. q  e.  NN0  suc  k  e.  dom  ( H `  q
) ) )
74 fveq2 5534 . . . . . . . . 9  |-  ( i  =  q  ->  ( H `  i )  =  ( H `  q ) )
7574dmeqd 4847 . . . . . . . 8  |-  ( i  =  q  ->  dom  ( H `  i )  =  dom  ( H `
 q ) )
7675eleq2d 2259 . . . . . . 7  |-  ( i  =  q  ->  ( suc  k  e.  dom  ( H `  i )  <->  suc  k  e.  dom  ( H `  q ) ) )
7776cbvrexv 2719 . . . . . 6  |-  ( E. i  e.  NN0  suc  k  e.  dom  ( H `
 i )  <->  E. q  e.  NN0  suc  k  e.  dom  ( H `  q
) )
7873, 77imbitrrdi 162 . . . . 5  |-  ( (
ph  /\  k  e.  om )  ->  ( E. i  e.  NN0  k  e. 
dom  ( H `  i )  ->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i
) ) )
7978expcom 116 . . . 4  |-  ( k  e.  om  ->  ( ph  ->  ( E. i  e.  NN0  k  e.  dom  ( H `  i )  ->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i )
) ) )
8079a2d 26 . . 3  |-  ( k  e.  om  ->  (
( ph  ->  E. i  e.  NN0  k  e.  dom  ( H `  i ) )  ->  ( ph  ->  E. i  e.  NN0  suc  k  e.  dom  ( H `  i )
) ) )
814, 7, 10, 13, 41, 80finds 4617 . 2  |-  ( M  e.  om  ->  ( ph  ->  E. i  e.  NN0  M  e.  dom  ( H `
 i ) ) )
821, 81mpcom 36 1  |-  ( ph  ->  E. i  e.  NN0  M  e.  dom  ( H `
 i ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105  DECID wdc 835    = wceq 1364    e. wcel 2160    =/= wne 2360   A.wral 2468   E.wrex 2469    u. cun 3142    C_ wss 3144   (/)c0 3437   ifcif 3549   {csn 3607   <.cop 3610    |-> cmpt 4079   Ord word 4380   suc csuc 4383   omcom 4607   `'ccnv 4643   dom cdm 4644   "cima 4647    Fn wfn 5230   -->wf 5231   -onto->wfo 5233   ` cfv 5235  (class class class)co 5897    e. cmpo 5899  freccfrec 6416    ^pm cpm 6676   0cc0 7842   1c1 7843    + caddc 7845    - cmin 8159   NN0cn0 9207   ZZcz 9284    seqcseq 10478
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-iinf 4605  ax-cnex 7933  ax-resscn 7934  ax-1cn 7935  ax-1re 7936  ax-icn 7937  ax-addcl 7938  ax-addrcl 7939  ax-mulcl 7940  ax-addcom 7942  ax-addass 7944  ax-distr 7946  ax-i2m1 7947  ax-0lt1 7948  ax-0id 7950  ax-rnegex 7951  ax-cnre 7953  ax-pre-ltirr 7954  ax-pre-ltwlin 7955  ax-pre-lttrn 7956  ax-pre-ltadd 7958
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4311  df-iord 4384  df-on 4386  df-ilim 4387  df-suc 4389  df-iom 4608  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-f1 5240  df-fo 5241  df-f1o 5242  df-fv 5243  df-riota 5852  df-ov 5900  df-oprab 5901  df-mpo 5902  df-1st 6166  df-2nd 6167  df-recs 6331  df-frec 6417  df-pm 6678  df-pnf 8025  df-mnf 8026  df-xr 8027  df-ltxr 8028  df-le 8029  df-sub 8161  df-neg 8162  df-inn 8951  df-n0 9208  df-z 9285  df-uz 9560  df-seqfrec 10479
This theorem is referenced by:  ennnfonelemdm  12474
  Copyright terms: Public domain W3C validator