xnn0nnen - Intuitionistic Logic Explorer

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

Theorem xnn0nnen 10604

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	⊢ ℕ₀^* ≈ ℕ

**Proof of Theorem xnn0nnen**
Step	Hyp	Ref	Expression
1		fnresi 5403	. . . . . . . 8 ⊢ ( I ↾ ℕ₀) Fn ℕ₀
2		pnfex 8146	. . . . . . . . 9 ⊢ +∞ ∈ V
3		neg1z 9424	. . . . . . . . . 10 ⊢ -1 ∈ ℤ
4	3	elexi 2786	. . . . . . . . 9 ⊢ -1 ∈ V
5	2, 4	fnsn 5337	. . . . . . . 8 ⊢ {⟨+∞, -1⟩} Fn {+∞}
6	1, 5	pm3.2i 272	. . . . . . 7 ⊢ (( I ↾ ℕ₀) Fn ℕ₀ ∧ {⟨+∞, -1⟩} Fn {+∞})
7		disj 3513	. . . . . . . 8 ⊢ ((ℕ₀ ∩ {+∞}) = ∅ ↔ ∀𝑥 ∈ ℕ₀ ¬ 𝑥 ∈ {+∞})
8		nn0nepnf 9386	. . . . . . . . 9 ⊢ (𝑥 ∈ ℕ₀ → 𝑥 ≠ +∞)
9		nelsn 3673	. . . . . . . . 9 ⊢ (𝑥 ≠ +∞ → ¬ 𝑥 ∈ {+∞})
10	8, 9	syl 14	. . . . . . . 8 ⊢ (𝑥 ∈ ℕ₀ → ¬ 𝑥 ∈ {+∞})
11	7, 10	mprgbir 2565	. . . . . . 7 ⊢ (ℕ₀ ∩ {+∞}) = ∅
12		fnun 5391	. . . . . . 7 ⊢ (((( I ↾ ℕ₀) Fn ℕ₀ ∧ {⟨+∞, -1⟩} Fn {+∞}) ∧ (ℕ₀ ∩ {+∞}) = ∅) → (( I ↾ ℕ₀) ∪ {⟨+∞, -1⟩}) Fn (ℕ₀ ∪ {+∞}))
13	6, 11, 12	mp2an 426	. . . . . 6 ⊢ (( I ↾ ℕ₀) ∪ {⟨+∞, -1⟩}) Fn (ℕ₀ ∪ {+∞})
14		uncom 3321	. . . . . . 7 ⊢ (( I ↾ ℕ₀) ∪ {⟨+∞, -1⟩}) = ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀))
15		df-xnn0 9379	. . . . . . . 8 ⊢ ℕ₀^* = (ℕ₀ ∪ {+∞})
16	15	eqcomi 2210	. . . . . . 7 ⊢ (ℕ₀ ∪ {+∞}) = ℕ₀^*
17		fneq12 5376	. . . . . . 7 ⊢ (((( I ↾ ℕ₀) ∪ {⟨+∞, -1⟩}) = ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) ∧ (ℕ₀ ∪ {+∞}) = ℕ₀^) → ((( I ↾ ℕ₀) ∪ {⟨+∞, -1⟩}) Fn (ℕ₀ ∪ {+∞}) ↔ ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ℕ₀^))
18	14, 16, 17	mp2an 426	. . . . . 6 ⊢ ((( I ↾ ℕ₀) ∪ {⟨+∞, -1⟩}) Fn (ℕ₀ ∪ {+∞}) ↔ ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ℕ₀^*)
19	13, 18	mpbi 145	. . . . 5 ⊢ ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ℕ₀^*
20	4, 2	fnsn 5337	. . . . . . . . . 10 ⊢ {⟨-1, +∞⟩} Fn {-1}
21	20, 1	pm3.2i 272	. . . . . . . . 9 ⊢ ({⟨-1, +∞⟩} Fn {-1} ∧ ( I ↾ ℕ₀) Fn ℕ₀)
22		disj 3513	. . . . . . . . . 10 ⊢ (({-1} ∩ ℕ₀) = ∅ ↔ ∀𝑥 ∈ {-1} ¬ 𝑥 ∈ ℕ₀)
23		neg1lt0 9164	. . . . . . . . . . . 12 ⊢ -1 < 0
24		nn0nlt0 9341	. . . . . . . . . . . 12 ⊢ (-1 ∈ ℕ₀ → ¬ -1 < 0)
25	23, 24	mt2 641	. . . . . . . . . . 11 ⊢ ¬ -1 ∈ ℕ₀
26		elsni 3656	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ {-1} → 𝑥 = -1)
27	26	eleq1d 2275	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {-1} → (𝑥 ∈ ℕ₀ ↔ -1 ∈ ℕ₀))
28	25, 27	mtbiri 677	. . . . . . . . . 10 ⊢ (𝑥 ∈ {-1} → ¬ 𝑥 ∈ ℕ₀)
29	22, 28	mprgbir 2565	. . . . . . . . 9 ⊢ ({-1} ∩ ℕ₀) = ∅
30		fnun 5391	. . . . . . . . 9 ⊢ ((({⟨-1, +∞⟩} Fn {-1} ∧ ( I ↾ ℕ₀) Fn ℕ₀) ∧ ({-1} ∩ ℕ₀) = ∅) → ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ₀)) Fn ({-1} ∪ ℕ₀))
31	21, 29, 30	mp2an 426	. . . . . . . 8 ⊢ ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ₀)) Fn ({-1} ∪ ℕ₀)
32		cnvun 5097	. . . . . . . . . 10 ⊢ ^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) = (^◡{⟨+∞, -1⟩} ∪ ^◡( I ↾ ℕ₀))
33	2, 4	cnvsn 5174	. . . . . . . . . . 11 ⊢ ^◡{⟨+∞, -1⟩} = {⟨-1, +∞⟩}
34		cnvresid 5357	. . . . . . . . . . 11 ⊢ ^◡( I ↾ ℕ₀) = ( I ↾ ℕ₀)
35	33, 34	uneq12i 3329	. . . . . . . . . 10 ⊢ (^◡{⟨+∞, -1⟩} ∪ ^◡( I ↾ ℕ₀)) = ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ₀))
36	32, 35	eqtri 2227	. . . . . . . . 9 ⊢ ^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) = ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ₀))
37	36	fneq1i 5377	. . . . . . . 8 ⊢ (^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ({-1} ∪ ℕ₀) ↔ ({⟨-1, +∞⟩} ∪ ( I ↾ ℕ₀)) Fn ({-1} ∪ ℕ₀))
38	31, 37	mpbir 146	. . . . . . 7 ⊢ ^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ({-1} ∪ ℕ₀)
39		fzosn 10356	. . . . . . . . . . 11 ⊢ (-1 ∈ ℤ → (-1..^(-1 + 1)) = {-1})
40	3, 39	ax-mp 5	. . . . . . . . . 10 ⊢ (-1..^(-1 + 1)) = {-1}
41		ax-1cn 8038	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
42	41, 41	negsubdii 8377	. . . . . . . . . . . 12 ⊢ -(1 − 1) = (-1 + 1)
43		1m1e0 9125	. . . . . . . . . . . . 13 ⊢ (1 − 1) = 0
44	41, 41	subcli 8368	. . . . . . . . . . . . . 14 ⊢ (1 − 1) ∈ ℂ
45		negeq0 8346	. . . . . . . . . . . . . 14 ⊢ ((1 − 1) ∈ ℂ → ((1 − 1) = 0 ↔ -(1 − 1) = 0))
46	44, 45	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ((1 − 1) = 0 ↔ -(1 − 1) = 0)
47	43, 46	mpbi 145	. . . . . . . . . . . 12 ⊢ -(1 − 1) = 0
48	42, 47	eqtr3i 2229	. . . . . . . . . . 11 ⊢ (-1 + 1) = 0
49	48	oveq2i 5968	. . . . . . . . . 10 ⊢ (-1..^(-1 + 1)) = (-1..^0)
50	40, 49	eqtr3i 2229	. . . . . . . . 9 ⊢ {-1} = (-1..^0)
51		nn0uz 9703	. . . . . . . . 9 ⊢ ℕ₀ = (ℤ_≥‘0)
52	50, 51	uneq12i 3329	. . . . . . . 8 ⊢ ({-1} ∪ ℕ₀) = ((-1..^0) ∪ (ℤ_≥‘0))
53	52	fneq2i 5378	. . . . . . 7 ⊢ (^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ({-1} ∪ ℕ₀) ↔ ^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ((-1..^0) ∪ (ℤ_≥‘0)))
54	38, 53	mpbi 145	. . . . . 6 ⊢ ^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ((-1..^0) ∪ (ℤ_≥‘0))
55		0z 9403	. . . . . . . . 9 ⊢ 0 ∈ ℤ
56		neg1rr 9162	. . . . . . . . . 10 ⊢ -1 ∈ ℝ
57		0re 8092	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
58	56, 57, 23	ltleii 8195	. . . . . . . . 9 ⊢ -1 ≤ 0
59		eluz2 9674	. . . . . . . . 9 ⊢ (0 ∈ (ℤ_≥‘-1) ↔ (-1 ∈ ℤ ∧ 0 ∈ ℤ ∧ -1 ≤ 0))
60	3, 55, 58, 59	mpbir3an 1182	. . . . . . . 8 ⊢ 0 ∈ (ℤ_≥‘-1)
61		fzouzsplit 10323	. . . . . . . 8 ⊢ (0 ∈ (ℤ_≥‘-1) → (ℤ_≥‘-1) = ((-1..^0) ∪ (ℤ_≥‘0)))
62	60, 61	ax-mp 5	. . . . . . 7 ⊢ (ℤ_≥‘-1) = ((-1..^0) ∪ (ℤ_≥‘0))
63	62	fneq2i 5378	. . . . . 6 ⊢ (^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn (ℤ_≥‘-1) ↔ ^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ((-1..^0) ∪ (ℤ_≥‘0)))
64	54, 63	mpbir 146	. . . . 5 ⊢ ^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn (ℤ_≥‘-1)
65	19, 64	pm3.2i 272	. . . 4 ⊢ (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ℕ₀^* ∧ ^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn (ℤ_≥‘-1))
66		dff1o4 5542	. . . 4 ⊢ (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)):ℕ₀^–1-1-onto→(ℤ_≥‘-1) ↔ (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn ℕ₀^ ∧ ^◡({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)) Fn (ℤ_≥‘-1)))
67	65, 66	mpbir 146	. . 3 ⊢ ({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)):ℕ₀^*–1-1-onto→(ℤ_≥‘-1)
68		nn0ex 9321	. . . . . 6 ⊢ ℕ₀ ∈ V
69	2	snex 4237	. . . . . 6 ⊢ {+∞} ∈ V
70	68, 69	unex 4496	. . . . 5 ⊢ (ℕ₀ ∪ {+∞}) ∈ V
71	15, 70	eqeltri 2279	. . . 4 ⊢ ℕ₀^* ∈ V
72	71	f1oen 6863	. . 3 ⊢ (({⟨+∞, -1⟩} ∪ ( I ↾ ℕ₀)):ℕ₀^–1-1-onto→(ℤ_≥‘-1) → ℕ₀^ ≈ (ℤ_≥‘-1))
73	67, 72	ax-mp 5	. 2 ⊢ ℕ₀^* ≈ (ℤ_≥‘-1)
74		uzennn 10603	. . 3 ⊢ (-1 ∈ ℤ → (ℤ_≥‘-1) ≈ ℕ)
75	3, 74	ax-mp 5	. 2 ⊢ (ℤ_≥‘-1) ≈ ℕ
76	73, 75	entri 6891	1 ⊢ ℕ₀^* ≈ ℕ

Colors of variables: wff set class

Syntax hints: ¬ wn 3 ∧ wa 104 ↔ wb 105 = wceq 1373 ∈ wcel 2177 ≠ wne 2377 Vcvv 2773 ∪ cun 3168 ∩ cin 3169 ∅c0 3464 {csn 3638 ⟨cop 3641 class class class wbr 4051 I cid 4343 ^◡ccnv 4682 ↾ cres 4685 Fn wfn 5275 –1-1-onto→wf1o 5279 ‘cfv 5280 (class class class)co 5957 ≈ cen 6838 ℂcc 7943 0cc0 7945 1c1 7946 + caddc 7948 +∞cpnf 8124 < clt 8127 ≤ cle 8128 − cmin 8263 -cneg 8264 ℕcn 9056 ℕ₀cn0 9315 ℕ₀^*cxnn0 9378 ℤcz 9392 ℤ_≥cuz 9668 ..^cfzo 10284

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-coll 4167 ax-sep 4170 ax-pow 4226 ax-pr 4261 ax-un 4488 ax-setind 4593 ax-cnex 8036 ax-resscn 8037 ax-1cn 8038 ax-1re 8039 ax-icn 8040 ax-addcl 8041 ax-addrcl 8042 ax-mulcl 8043 ax-addcom 8045 ax-addass 8047 ax-distr 8049 ax-i2m1 8050 ax-0lt1 8051 ax-0id 8053 ax-rnegex 8054 ax-cnre 8056 ax-pre-ltirr 8057 ax-pre-ltwlin 8058 ax-pre-lttrn 8059 ax-pre-apti 8060 ax-pre-ltadd 8061

This theorem depends on definitions: df-bi 117 df-3or 982 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-nel 2473 df-ral 2490 df-rex 2491 df-reu 2492 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-nul 3465 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3857 df-int 3892 df-iun 3935 df-br 4052 df-opab 4114 df-mpt 4115 df-id 4348 df-xp 4689 df-rel 4690 df-cnv 4691 df-co 4692 df-dm 4693 df-rn 4694 df-res 4695 df-ima 4696 df-iota 5241 df-fun 5282 df-fn 5283 df-f 5284 df-f1 5285 df-fo 5286 df-f1o 5287 df-fv 5288 df-riota 5912 df-ov 5960 df-oprab 5961 df-mpo 5962 df-1st 6239 df-2nd 6240 df-er 6633 df-en 6841 df-pnf 8129 df-mnf 8130 df-xr 8131 df-ltxr 8132 df-le 8133 df-sub 8265 df-neg 8266 df-inn 9057 df-n0 9316 df-xnn0 9379 df-z 9393 df-uz 9669 df-fz 10151 df-fzo 10285

This theorem is referenced by: nninfct 12437

W3C validator