![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0tonninf | GIF version |
Description: The mapping of zero into ℕ∞ is the sequence of all zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.) |
Ref | Expression |
---|---|
fxnn0nninf.g | ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) |
fxnn0nninf.f | ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) |
fxnn0nninf.i | ⊢ 𝐼 = ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}) |
Ref | Expression |
---|---|
0tonninf | ⊢ (𝐼‘0) = (𝑥 ∈ ω ↦ ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fxnn0nninf.i | . . . . 5 ⊢ 𝐼 = ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}) | |
2 | 1 | fveq1i 5535 | . . . 4 ⊢ (𝐼‘0) = (((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉})‘0) |
3 | 0xnn0 9275 | . . . . 5 ⊢ 0 ∈ ℕ0* | |
4 | 0nn0 9221 | . . . . . . 7 ⊢ 0 ∈ ℕ0 | |
5 | nn0nepnf 9277 | . . . . . . 7 ⊢ (0 ∈ ℕ0 → 0 ≠ +∞) | |
6 | 4, 5 | ax-mp 5 | . . . . . 6 ⊢ 0 ≠ +∞ |
7 | 6 | necomi 2445 | . . . . 5 ⊢ +∞ ≠ 0 |
8 | fvunsng 5731 | . . . . 5 ⊢ ((0 ∈ ℕ0* ∧ +∞ ≠ 0) → (((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉})‘0) = ((𝐹 ∘ ◡𝐺)‘0)) | |
9 | 3, 7, 8 | mp2an 426 | . . . 4 ⊢ (((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉})‘0) = ((𝐹 ∘ ◡𝐺)‘0) |
10 | fxnn0nninf.g | . . . . . . . 8 ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) | |
11 | 10 | frechashgf1o 10459 | . . . . . . 7 ⊢ 𝐺:ω–1-1-onto→ℕ0 |
12 | f1ocnv 5493 | . . . . . . 7 ⊢ (𝐺:ω–1-1-onto→ℕ0 → ◡𝐺:ℕ0–1-1-onto→ω) | |
13 | 11, 12 | ax-mp 5 | . . . . . 6 ⊢ ◡𝐺:ℕ0–1-1-onto→ω |
14 | f1of 5480 | . . . . . 6 ⊢ (◡𝐺:ℕ0–1-1-onto→ω → ◡𝐺:ℕ0⟶ω) | |
15 | 13, 14 | ax-mp 5 | . . . . 5 ⊢ ◡𝐺:ℕ0⟶ω |
16 | fvco3 5608 | . . . . 5 ⊢ ((◡𝐺:ℕ0⟶ω ∧ 0 ∈ ℕ0) → ((𝐹 ∘ ◡𝐺)‘0) = (𝐹‘(◡𝐺‘0))) | |
17 | 15, 4, 16 | mp2an 426 | . . . 4 ⊢ ((𝐹 ∘ ◡𝐺)‘0) = (𝐹‘(◡𝐺‘0)) |
18 | 2, 9, 17 | 3eqtri 2214 | . . 3 ⊢ (𝐼‘0) = (𝐹‘(◡𝐺‘0)) |
19 | 0zd 9295 | . . . . . . 7 ⊢ (⊤ → 0 ∈ ℤ) | |
20 | 19, 10 | frec2uz0d 10430 | . . . . . 6 ⊢ (⊤ → (𝐺‘∅) = 0) |
21 | 20 | mptru 1373 | . . . . 5 ⊢ (𝐺‘∅) = 0 |
22 | peano1 4611 | . . . . . 6 ⊢ ∅ ∈ ω | |
23 | f1ocnvfv 5801 | . . . . . 6 ⊢ ((𝐺:ω–1-1-onto→ℕ0 ∧ ∅ ∈ ω) → ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅)) | |
24 | 11, 22, 23 | mp2an 426 | . . . . 5 ⊢ ((𝐺‘∅) = 0 → (◡𝐺‘0) = ∅) |
25 | 21, 24 | ax-mp 5 | . . . 4 ⊢ (◡𝐺‘0) = ∅ |
26 | 25 | fveq2i 5537 | . . 3 ⊢ (𝐹‘(◡𝐺‘0)) = (𝐹‘∅) |
27 | eleq2 2253 | . . . . . . 7 ⊢ (𝑛 = ∅ → (𝑖 ∈ 𝑛 ↔ 𝑖 ∈ ∅)) | |
28 | 27 | ifbid 3570 | . . . . . 6 ⊢ (𝑛 = ∅ → if(𝑖 ∈ 𝑛, 1o, ∅) = if(𝑖 ∈ ∅, 1o, ∅)) |
29 | 28 | mpteq2dv 4109 | . . . . 5 ⊢ (𝑛 = ∅ → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) = (𝑖 ∈ ω ↦ if(𝑖 ∈ ∅, 1o, ∅))) |
30 | fxnn0nninf.f | . . . . 5 ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) | |
31 | omex 4610 | . . . . . 6 ⊢ ω ∈ V | |
32 | 31 | mptex 5763 | . . . . 5 ⊢ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)) ∈ V |
33 | 29, 30, 32 | fvmpt3i 5617 | . . . 4 ⊢ (∅ ∈ ω → (𝐹‘∅) = (𝑖 ∈ ω ↦ if(𝑖 ∈ ∅, 1o, ∅))) |
34 | 22, 33 | ax-mp 5 | . . 3 ⊢ (𝐹‘∅) = (𝑖 ∈ ω ↦ if(𝑖 ∈ ∅, 1o, ∅)) |
35 | 18, 26, 34 | 3eqtri 2214 | . 2 ⊢ (𝐼‘0) = (𝑖 ∈ ω ↦ if(𝑖 ∈ ∅, 1o, ∅)) |
36 | noel 3441 | . . . 4 ⊢ ¬ 𝑖 ∈ ∅ | |
37 | 36 | iffalsei 3558 | . . 3 ⊢ if(𝑖 ∈ ∅, 1o, ∅) = ∅ |
38 | 37 | mpteq2i 4105 | . 2 ⊢ (𝑖 ∈ ω ↦ if(𝑖 ∈ ∅, 1o, ∅)) = (𝑖 ∈ ω ↦ ∅) |
39 | eqidd 2190 | . . 3 ⊢ (𝑖 = 𝑥 → ∅ = ∅) | |
40 | 39 | cbvmptv 4114 | . 2 ⊢ (𝑖 ∈ ω ↦ ∅) = (𝑥 ∈ ω ↦ ∅) |
41 | 35, 38, 40 | 3eqtri 2214 | 1 ⊢ (𝐼‘0) = (𝑥 ∈ ω ↦ ∅) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1364 ⊤wtru 1365 ∈ wcel 2160 ≠ wne 2360 ∪ cun 3142 ∅c0 3437 ifcif 3549 {csn 3607 〈cop 3610 ↦ cmpt 4079 ωcom 4607 × cxp 4642 ◡ccnv 4643 ∘ ccom 4648 ⟶wf 5231 –1-1-onto→wf1o 5234 ‘cfv 5235 (class class class)co 5896 freccfrec 6415 1oc1o 6434 0cc0 7841 1c1 7842 + caddc 7844 +∞cpnf 8019 ℕ0cn0 9206 ℕ0*cxnn0 9269 ℤcz 9283 |
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 7932 ax-resscn 7933 ax-1cn 7934 ax-1re 7935 ax-icn 7936 ax-addcl 7937 ax-addrcl 7938 ax-mulcl 7939 ax-addcom 7941 ax-addass 7943 ax-distr 7945 ax-i2m1 7946 ax-0lt1 7947 ax-0id 7949 ax-rnegex 7950 ax-cnre 7952 ax-pre-ltirr 7953 ax-pre-ltwlin 7954 ax-pre-lttrn 7955 ax-pre-ltadd 7957 |
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 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 5899 df-oprab 5900 df-mpo 5901 df-recs 6330 df-frec 6416 df-pnf 8024 df-mnf 8025 df-xr 8026 df-ltxr 8027 df-le 8028 df-sub 8160 df-neg 8161 df-inn 8950 df-n0 9207 df-xnn0 9270 df-z 9284 df-uz 9559 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |