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

Theorem nninfisol 7150
Description: Finite elements of ℕ are isolated. That is, given a natural number and any element of ℕ, it is decidable whether the natural number (when converted to an element of ℕ) is equal to the given element of ℕ. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence  X to decide whether it is equal to  N (in fact, you only need to look at two elements and  N tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
Assertion
Ref Expression
nninfisol  |-  ( ( N  e.  om  /\  X  e. )  -> DECID  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
Distinct variable groups:    i, N    i, X

Proof of Theorem nninfisol
StepHypRef Expression
1 simpllr 534 . . . 4  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  N  =  (/) )  ->  X  e. )
2 simplr 528 . . . 4  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  N  =  (/) )  ->  ( X `  N )  =  (/) )
3 simplll 533 . . . 4  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  N  =  (/) )  ->  N  e.  om )
4 simpr 110 . . . 4  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  N  =  (/) )  ->  N  =  (/) )
51, 2, 3, 4nninfisollem0 7147 . . 3  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  N  =  (/) )  -> DECID  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
6 simp-4r 542 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  (/) )  ->  X  e. )
7 simpllr 534 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  (/) )  ->  ( X `  N )  =  (/) )
8 simp-4l 541 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  (/) )  ->  N  e.  om )
9 simpr 110 . . . . . . 7  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  ->  -.  N  =  (/) )
109neqned 2367 . . . . . 6  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  ->  N  =/=  (/) )
1110adantr 276 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  (/) )  ->  N  =/=  (/) )
12 simpr 110 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  (/) )  ->  ( X `  U. N )  =  (/) )
136, 7, 8, 11, 12nninfisollemne 7148 . . . 4  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  (/) )  -> DECID  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
14 simp-4r 542 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  1o )  ->  X  e. )
15 simpllr 534 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  1o )  -> 
( X `  N
)  =  (/) )
16 simp-4l 541 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  1o )  ->  N  e.  om )
1710adantr 276 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  1o )  ->  N  =/=  (/) )
18 simpr 110 . . . . 5  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  1o )  -> 
( X `  U. N )  =  1o )
1914, 15, 16, 17, 18nninfisollemeq 7149 . . . 4  |-  ( ( ( ( ( N  e.  om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  /\  ( X `  U. N )  =  1o )  -> DECID  (
i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
20 nninff 7140 . . . . . . . . 9  |-  ( X  e.  ->  X : om --> 2o )
2120adantl 277 . . . . . . . 8  |-  ( ( N  e.  om  /\  X  e. )  ->  X : om
--> 2o )
22 nnpredcl 4637 . . . . . . . . 9  |-  ( N  e.  om  ->  U. N  e.  om )
2322adantr 276 . . . . . . . 8  |-  ( ( N  e.  om  /\  X  e. )  ->  U. N  e. 
om )
2421, 23ffvelcdmd 5668 . . . . . . 7  |-  ( ( N  e.  om  /\  X  e. )  ->  ( X `  U. N )  e.  2o )
25 df2o3 6449 . . . . . . 7  |-  2o  =  { (/) ,  1o }
2624, 25eleqtrdi 2282 . . . . . 6  |-  ( ( N  e.  om  /\  X  e. )  ->  ( X `  U. N )  e. 
{ (/) ,  1o }
)
27 elpri 3630 . . . . . 6  |-  ( ( X `  U. N
)  e.  { (/) ,  1o }  ->  (
( X `  U. N )  =  (/)  \/  ( X `  U. N )  =  1o ) )
2826, 27syl 14 . . . . 5  |-  ( ( N  e.  om  /\  X  e. )  ->  ( ( X `  U. N )  =  (/)  \/  ( X `  U. N )  =  1o ) )
2928ad2antrr 488 . . . 4  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  -> 
( ( X `  U. N )  =  (/)  \/  ( X `  U. N )  =  1o ) )
3013, 19, 29mpjaodan 799 . . 3  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  (/) )  /\  -.  N  =  (/) )  -> DECID  (
i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
31 nndceq0 4632 . . . . 5  |-  ( N  e.  om  -> DECID  N  =  (/) )
32 exmiddc 837 . . . . 5  |-  (DECID  N  =  (/)  ->  ( N  =  (/)  \/  -.  N  =  (/) ) )
3331, 32syl 14 . . . 4  |-  ( N  e.  om  ->  ( N  =  (/)  \/  -.  N  =  (/) ) )
3433ad2antrr 488 . . 3  |-  ( ( ( N  e.  om  /\  X  e. )  /\  ( X `
 N )  =  (/) )  ->  ( N  =  (/)  \/  -.  N  =  (/) ) )
355, 30, 34mpjaodan 799 . 2  |-  ( ( ( N  e.  om  /\  X  e. )  /\  ( X `
 N )  =  (/) )  -> DECID  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
36 1n0 6451 . . . . . 6  |-  1o  =/=  (/)
3736neii 2362 . . . . 5  |-  -.  1o  =  (/)
38 simpr 110 . . . . . . . 8  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  1o )  /\  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )  -> 
( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
3938fveq1d 5532 . . . . . . 7  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  1o )  /\  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )  -> 
( ( i  e. 
om  |->  if ( i  e.  N ,  1o ,  (/) ) ) `  N )  =  ( X `  N ) )
40 eqid 2189 . . . . . . . . . 10  |-  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  ( i  e. 
om  |->  if ( i  e.  N ,  1o ,  (/) ) )
41 eleq1 2252 . . . . . . . . . . 11  |-  ( i  =  N  ->  (
i  e.  N  <->  N  e.  N ) )
4241ifbid 3570 . . . . . . . . . 10  |-  ( i  =  N  ->  if ( i  e.  N ,  1o ,  (/) )  =  if ( N  e.  N ,  1o ,  (/) ) )
43 id 19 . . . . . . . . . 10  |-  ( N  e.  om  ->  N  e.  om )
44 nnord 4626 . . . . . . . . . . . . 13  |-  ( N  e.  om  ->  Ord  N )
45 ordirr 4556 . . . . . . . . . . . . 13  |-  ( Ord 
N  ->  -.  N  e.  N )
4644, 45syl 14 . . . . . . . . . . . 12  |-  ( N  e.  om  ->  -.  N  e.  N )
4746iffalsed 3559 . . . . . . . . . . 11  |-  ( N  e.  om  ->  if ( N  e.  N ,  1o ,  (/) )  =  (/) )
48 peano1 4608 . . . . . . . . . . 11  |-  (/)  e.  om
4947, 48eqeltrdi 2280 . . . . . . . . . 10  |-  ( N  e.  om  ->  if ( N  e.  N ,  1o ,  (/) )  e. 
om )
5040, 42, 43, 49fvmptd3 5625 . . . . . . . . 9  |-  ( N  e.  om  ->  (
( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) ) `
 N )  =  if ( N  e.  N ,  1o ,  (/) ) )
5150, 47eqtrd 2222 . . . . . . . 8  |-  ( N  e.  om  ->  (
( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) ) `
 N )  =  (/) )
5251ad3antrrr 492 . . . . . . 7  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  1o )  /\  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )  -> 
( ( i  e. 
om  |->  if ( i  e.  N ,  1o ,  (/) ) ) `  N )  =  (/) )
53 simplr 528 . . . . . . 7  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  1o )  /\  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )  -> 
( X `  N
)  =  1o )
5439, 52, 533eqtr3rd 2231 . . . . . 6  |-  ( ( ( ( N  e. 
om  /\  X  e. )  /\  ( X `  N )  =  1o )  /\  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )  ->  1o  =  (/) )
5554ex 115 . . . . 5  |-  ( ( ( N  e.  om  /\  X  e. )  /\  ( X `
 N )  =  1o )  ->  (
( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X  ->  1o  =  (/) ) )
5637, 55mtoi 665 . . . 4  |-  ( ( ( N  e.  om  /\  X  e. )  /\  ( X `
 N )  =  1o )  ->  -.  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
5756olcd 735 . . 3  |-  ( ( ( N  e.  om  /\  X  e. )  /\  ( X `
 N )  =  1o )  ->  (
( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X  \/  -.  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X ) )
58 df-dc 836 . . 3  |-  (DECID  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X  <->  ( (
i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X  \/  -.  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X ) )
5957, 58sylibr 134 . 2  |-  ( ( ( N  e.  om  /\  X  e. )  /\  ( X `
 N )  =  1o )  -> DECID  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
60 simpl 109 . . . . 5  |-  ( ( N  e.  om  /\  X  e. )  ->  N  e.  om )
6121, 60ffvelcdmd 5668 . . . 4  |-  ( ( N  e.  om  /\  X  e. )  ->  ( X `  N )  e.  2o )
6261, 25eleqtrdi 2282 . . 3  |-  ( ( N  e.  om  /\  X  e. )  ->  ( X `  N )  e.  { (/)
,  1o } )
63 elpri 3630 . . 3  |-  ( ( X `  N )  e.  { (/) ,  1o }  ->  ( ( X `
 N )  =  (/)  \/  ( X `  N )  =  1o ) )
6462, 63syl 14 . 2  |-  ( ( N  e.  om  /\  X  e. )  ->  ( ( X `  N )  =  (/)  \/  ( X `
 N )  =  1o ) )
6535, 59, 64mpjaodan 799 1  |-  ( ( N  e.  om  /\  X  e. )  -> DECID  ( i  e.  om  |->  if ( i  e.  N ,  1o ,  (/) ) )  =  X )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    \/ wo 709  DECID wdc 835    = wceq 1364    e. wcel 2160    =/= wne 2360   (/)c0 3437   ifcif 3549   {cpr 3608   U.cuni 3824    |-> cmpt 4079   Ord word 4377   omcom 4604   -->wf 5227   ` cfv 5231   1oc1o 6428   2oc2o 6429  ℕxnninf 7137
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-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602
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-ral 2473  df-rex 2474  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-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-id 4308  df-iord 4381  df-on 4383  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-fv 5239  df-ov 5894  df-oprab 5895  df-mpo 5896  df-1o 6435  df-2o 6436  df-map 6668  df-nninf 7138
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator