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

Theorem xnn0nnen 10508
Description: The set of extended nonnegative integers is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 14-Jul-2025.)
Assertion
Ref Expression
xnn0nnen 0* ≈ ℕ

Proof of Theorem xnn0nnen
StepHypRef Expression
1 fnresi 5371 . . . . . . . 8 ( I ↾ ℕ0) Fn ℕ0
2 pnfex 8073 . . . . . . . . 9 +∞ ∈ V
3 neg1z 9349 . . . . . . . . . 10 -1 ∈ ℤ
43elexi 2772 . . . . . . . . 9 -1 ∈ V
52, 4fnsn 5308 . . . . . . . 8 {⟨+∞, -1⟩} Fn {+∞}
61, 5pm3.2i 272 . . . . . . 7 (( I ↾ ℕ0) Fn ℕ0 ∧ {⟨+∞, -1⟩} Fn {+∞})
7 disj 3495 . . . . . . . 8 ((ℕ0 ∩ {+∞}) = ∅ ↔ ∀𝑥 ∈ ℕ0 ¬ 𝑥 ∈ {+∞})
8 nn0nepnf 9311 . . . . . . . . 9 (𝑥 ∈ ℕ0𝑥 ≠ +∞)
9 nelsn 3653 . . . . . . . . 9 (𝑥 ≠ +∞ → ¬ 𝑥 ∈ {+∞})
108, 9syl 14 . . . . . . . 8 (𝑥 ∈ ℕ0 → ¬ 𝑥 ∈ {+∞})
117, 10mprgbir 2552 . . . . . . 7 (ℕ0 ∩ {+∞}) = ∅
12 fnun 5360 . . . . . . 7 (((( I ↾ ℕ0) Fn ℕ0 ∧ {⟨+∞, -1⟩} Fn {+∞}) ∧ (ℕ0 ∩ {+∞}) = ∅) → (( I ↾ ℕ0) ∪ {⟨+∞, -1⟩}) Fn (ℕ0 ∪ {+∞}))
136, 11, 12mp2an 426 . . . . . 6 (( I ↾ ℕ0) ∪ {⟨+∞, -1⟩}) Fn (ℕ0 ∪ {+∞})
14 uncom 3303 . . . . . . 7 (( I ↾ ℕ0) ∪ {⟨+∞, -1⟩}) = ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0))
15 df-xnn0 9304 . . . . . . . 8 0* = (ℕ0 ∪ {+∞})
1615eqcomi 2197 . . . . . . 7 (ℕ0 ∪ {+∞}) = ℕ0*
17 fneq12 5347 . . . . . . 7 (((( I ↾ ℕ0) ∪ {⟨+∞, -1⟩}) = ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) ∧ (ℕ0 ∪ {+∞}) = ℕ0*) → ((( I ↾ ℕ0) ∪ {⟨+∞, -1⟩}) Fn (ℕ0 ∪ {+∞}) ↔ ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ℕ0*))
1814, 16, 17mp2an 426 . . . . . 6 ((( I ↾ ℕ0) ∪ {⟨+∞, -1⟩}) Fn (ℕ0 ∪ {+∞}) ↔ ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ℕ0*)
1913, 18mpbi 145 . . . . 5 ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ℕ0*
204, 2fnsn 5308 . . . . . . . . . 10 {⟨-1, +∞⟩} Fn {-1}
2120, 1pm3.2i 272 . . . . . . . . 9 ({⟨-1, +∞⟩} Fn {-1} ∧ ( I ↾ ℕ0) Fn ℕ0)
22 disj 3495 . . . . . . . . . 10 (({-1} ∩ ℕ0) = ∅ ↔ ∀𝑥 ∈ {-1} ¬ 𝑥 ∈ ℕ0)
23 neg1lt0 9090 . . . . . . . . . . . 12 -1 < 0
24 nn0nlt0 9266 . . . . . . . . . . . 12 (-1 ∈ ℕ0 → ¬ -1 < 0)
2523, 24mt2 641 . . . . . . . . . . 11 ¬ -1 ∈ ℕ0
26 elsni 3636 . . . . . . . . . . . 12 (𝑥 ∈ {-1} → 𝑥 = -1)
2726eleq1d 2262 . . . . . . . . . . 11 (𝑥 ∈ {-1} → (𝑥 ∈ ℕ0 ↔ -1 ∈ ℕ0))
2825, 27mtbiri 676 . . . . . . . . . 10 (𝑥 ∈ {-1} → ¬ 𝑥 ∈ ℕ0)
2922, 28mprgbir 2552 . . . . . . . . 9 ({-1} ∩ ℕ0) = ∅
30 fnun 5360 . . . . . . . . 9 ((({⟨-1, +∞⟩} Fn {-1} ∧ ( I ↾ ℕ0) Fn ℕ0) ∧ ({-1} ∩ ℕ0) = ∅) → ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ0)) Fn ({-1} ∪ ℕ0))
3121, 29, 30mp2an 426 . . . . . . . 8 ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ0)) Fn ({-1} ∪ ℕ0)
32 cnvun 5071 . . . . . . . . . 10 ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) = ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0))
332, 4cnvsn 5148 . . . . . . . . . . 11 {⟨+∞, -1⟩} = {⟨-1, +∞⟩}
34 cnvresid 5328 . . . . . . . . . . 11 ( I ↾ ℕ0) = ( I ↾ ℕ0)
3533, 34uneq12i 3311 . . . . . . . . . 10 ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) = ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ0))
3632, 35eqtri 2214 . . . . . . . . 9 ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) = ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ0))
3736fneq1i 5348 . . . . . . . 8 (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ({-1} ∪ ℕ0) ↔ ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ0)) Fn ({-1} ∪ ℕ0))
3831, 37mpbir 146 . . . . . . 7 ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ({-1} ∪ ℕ0)
39 fzosn 10272 . . . . . . . . . . 11 (-1 ∈ ℤ → (-1..^(-1 + 1)) = {-1})
403, 39ax-mp 5 . . . . . . . . . 10 (-1..^(-1 + 1)) = {-1}
41 ax-1cn 7965 . . . . . . . . . . . . 13 1 ∈ ℂ
4241, 41negsubdii 8304 . . . . . . . . . . . 12 -(1 − 1) = (-1 + 1)
43 1m1e0 9051 . . . . . . . . . . . . 13 (1 − 1) = 0
4441, 41subcli 8295 . . . . . . . . . . . . . 14 (1 − 1) ∈ ℂ
45 negeq0 8273 . . . . . . . . . . . . . 14 ((1 − 1) ∈ ℂ → ((1 − 1) = 0 ↔ -(1 − 1) = 0))
4644, 45ax-mp 5 . . . . . . . . . . . . 13 ((1 − 1) = 0 ↔ -(1 − 1) = 0)
4743, 46mpbi 145 . . . . . . . . . . . 12 -(1 − 1) = 0
4842, 47eqtr3i 2216 . . . . . . . . . . 11 (-1 + 1) = 0
4948oveq2i 5929 . . . . . . . . . 10 (-1..^(-1 + 1)) = (-1..^0)
5040, 49eqtr3i 2216 . . . . . . . . 9 {-1} = (-1..^0)
51 nn0uz 9627 . . . . . . . . 9 0 = (ℤ‘0)
5250, 51uneq12i 3311 . . . . . . . 8 ({-1} ∪ ℕ0) = ((-1..^0) ∪ (ℤ‘0))
5352fneq2i 5349 . . . . . . 7 (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ({-1} ∪ ℕ0) ↔ ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ((-1..^0) ∪ (ℤ‘0)))
5438, 53mpbi 145 . . . . . 6 ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ((-1..^0) ∪ (ℤ‘0))
55 0z 9328 . . . . . . . . 9 0 ∈ ℤ
56 neg1rr 9088 . . . . . . . . . 10 -1 ∈ ℝ
57 0re 8019 . . . . . . . . . 10 0 ∈ ℝ
5856, 57, 23ltleii 8122 . . . . . . . . 9 -1 ≤ 0
59 eluz2 9598 . . . . . . . . 9 (0 ∈ (ℤ‘-1) ↔ (-1 ∈ ℤ ∧ 0 ∈ ℤ ∧ -1 ≤ 0))
603, 55, 58, 59mpbir3an 1181 . . . . . . . 8 0 ∈ (ℤ‘-1)
61 fzouzsplit 10246 . . . . . . . 8 (0 ∈ (ℤ‘-1) → (ℤ‘-1) = ((-1..^0) ∪ (ℤ‘0)))
6260, 61ax-mp 5 . . . . . . 7 (ℤ‘-1) = ((-1..^0) ∪ (ℤ‘0))
6362fneq2i 5349 . . . . . 6 (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn (ℤ‘-1) ↔ ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ((-1..^0) ∪ (ℤ‘0)))
6454, 63mpbir 146 . . . . 5 ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn (ℤ‘-1)
6519, 64pm3.2i 272 . . . 4 (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ℕ0*({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn (ℤ‘-1))
66 dff1o4 5508 . . . 4 (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)):ℕ0*1-1-onto→(ℤ‘-1) ↔ (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn ℕ0*({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)) Fn (ℤ‘-1)))
6765, 66mpbir 146 . . 3 ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)):ℕ0*1-1-onto→(ℤ‘-1)
68 nn0ex 9246 . . . . . 6 0 ∈ V
692snex 4214 . . . . . 6 {+∞} ∈ V
7068, 69unex 4472 . . . . 5 (ℕ0 ∪ {+∞}) ∈ V
7115, 70eqeltri 2266 . . . 4 0* ∈ V
7271f1oen 6813 . . 3 (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ0)):ℕ0*1-1-onto→(ℤ‘-1) → ℕ0* ≈ (ℤ‘-1))
7367, 72ax-mp 5 . 2 0* ≈ (ℤ‘-1)
74 uzennn 10507 . . 3 (-1 ∈ ℤ → (ℤ‘-1) ≈ ℕ)
753, 74ax-mp 5 . 2 (ℤ‘-1) ≈ ℕ
7673, 75entri 6840 1 0* ≈ ℕ
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 104  wb 105   = wceq 1364  wcel 2164  wne 2364  Vcvv 2760  cun 3151  cin 3152  c0 3446  {csn 3618  cop 3621   class class class wbr 4029   I cid 4319  ccnv 4658  cres 4661   Fn wfn 5249  1-1-ontowf1o 5253  cfv 5254  (class class class)co 5918  cen 6792  cc 7870  0cc0 7872  1c1 7873   + caddc 7875  +∞cpnf 8051   < clt 8054  cle 8055  cmin 8190  -cneg 8191  cn 8982  0cn0 9240  0*cxnn0 9303  cz 9317  cuz 9592  ..^cfzo 10208
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 2166  ax-14 2167  ax-ext 2175  ax-coll 4144  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-1cn 7965  ax-1re 7966  ax-icn 7967  ax-addcl 7968  ax-addrcl 7969  ax-mulcl 7970  ax-addcom 7972  ax-addass 7974  ax-distr 7976  ax-i2m1 7977  ax-0lt1 7978  ax-0id 7980  ax-rnegex 7981  ax-cnre 7983  ax-pre-ltirr 7984  ax-pre-ltwlin 7985  ax-pre-lttrn 7986  ax-pre-apti 7987  ax-pre-ltadd 7988
This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2986  df-csb 3081  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-int 3871  df-iun 3914  df-br 4030  df-opab 4091  df-mpt 4092  df-id 4324  df-xp 4665  df-rel 4666  df-cnv 4667  df-co 4668  df-dm 4669  df-rn 4670  df-res 4671  df-ima 4672  df-iota 5215  df-fun 5256  df-fn 5257  df-f 5258  df-f1 5259  df-fo 5260  df-f1o 5261  df-fv 5262  df-riota 5873  df-ov 5921  df-oprab 5922  df-mpo 5923  df-1st 6193  df-2nd 6194  df-er 6587  df-en 6795  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060  df-sub 8192  df-neg 8193  df-inn 8983  df-n0 9241  df-xnn0 9304  df-z 9318  df-uz 9593  df-fz 10075  df-fzo 10209
This theorem is referenced by:  nninfct  12178
  Copyright terms: Public domain W3C validator