Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fxnn0nninf | GIF version |
Description: A function from ℕ0* into ℕ∞. (Contributed by Jim Kingdon, 16-Jul-2022.) TODO: use infnninf 7104 instead of infnninfOLD 7105. More generally, this theorem and most theorems in this section could use an extended 𝐺 defined by 𝐺 = (frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) ∪ 〈ω, +∞〉) and 𝐹 = (𝑛 ∈ suc ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) as in nnnninf2 7107. |
Ref | Expression |
---|---|
fxnn0nninf.g | ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) |
fxnn0nninf.f | ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) |
fxnn0nninf.i | ⊢ 𝐼 = ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}) |
Ref | Expression |
---|---|
fxnn0nninf | ⊢ 𝐼:ℕ0*⟶ℕ∞ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fxnn0nninf.g | . . . . . 6 ⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0) | |
2 | fxnn0nninf.f | . . . . . 6 ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅))) | |
3 | 1, 2 | fnn0nninf 10397 | . . . . 5 ⊢ (𝐹 ∘ ◡𝐺):ℕ0⟶ℕ∞ |
4 | pnfex 7977 | . . . . . . . 8 ⊢ +∞ ∈ V | |
5 | omex 4578 | . . . . . . . . 9 ⊢ ω ∈ V | |
6 | 1oex 6407 | . . . . . . . . . 10 ⊢ 1o ∈ V | |
7 | 6 | snex 4172 | . . . . . . . . 9 ⊢ {1o} ∈ V |
8 | 5, 7 | xpex 4727 | . . . . . . . 8 ⊢ (ω × {1o}) ∈ V |
9 | 4, 8 | f1osn 5485 | . . . . . . 7 ⊢ {〈+∞, (ω × {1o})〉}:{+∞}–1-1-onto→{(ω × {1o})} |
10 | f1of 5445 | . . . . . . 7 ⊢ ({〈+∞, (ω × {1o})〉}:{+∞}–1-1-onto→{(ω × {1o})} → {〈+∞, (ω × {1o})〉}:{+∞}⟶{(ω × {1o})}) | |
11 | 9, 10 | ax-mp 5 | . . . . . 6 ⊢ {〈+∞, (ω × {1o})〉}:{+∞}⟶{(ω × {1o})} |
12 | infnninfOLD 7105 | . . . . . . 7 ⊢ (ω × {1o}) ∈ ℕ∞ | |
13 | snssi 3725 | . . . . . . 7 ⊢ ((ω × {1o}) ∈ ℕ∞ → {(ω × {1o})} ⊆ ℕ∞) | |
14 | 12, 13 | ax-mp 5 | . . . . . 6 ⊢ {(ω × {1o})} ⊆ ℕ∞ |
15 | fss 5361 | . . . . . 6 ⊢ (({〈+∞, (ω × {1o})〉}:{+∞}⟶{(ω × {1o})} ∧ {(ω × {1o})} ⊆ ℕ∞) → {〈+∞, (ω × {1o})〉}:{+∞}⟶ℕ∞) | |
16 | 11, 14, 15 | mp2an 424 | . . . . 5 ⊢ {〈+∞, (ω × {1o})〉}:{+∞}⟶ℕ∞ |
17 | 3, 16 | pm3.2i 270 | . . . 4 ⊢ ((𝐹 ∘ ◡𝐺):ℕ0⟶ℕ∞ ∧ {〈+∞, (ω × {1o})〉}:{+∞}⟶ℕ∞) |
18 | disj 3464 | . . . . 5 ⊢ ((ℕ0 ∩ {+∞}) = ∅ ↔ ∀𝑥 ∈ ℕ0 ¬ 𝑥 ∈ {+∞}) | |
19 | nn0nepnf 9210 | . . . . . . 7 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ≠ +∞) | |
20 | 19 | neneqd 2362 | . . . . . 6 ⊢ (𝑥 ∈ ℕ0 → ¬ 𝑥 = +∞) |
21 | elsni 3602 | . . . . . 6 ⊢ (𝑥 ∈ {+∞} → 𝑥 = +∞) | |
22 | 20, 21 | nsyl 624 | . . . . 5 ⊢ (𝑥 ∈ ℕ0 → ¬ 𝑥 ∈ {+∞}) |
23 | 18, 22 | mprgbir 2529 | . . . 4 ⊢ (ℕ0 ∩ {+∞}) = ∅ |
24 | fun2 5373 | . . . 4 ⊢ ((((𝐹 ∘ ◡𝐺):ℕ0⟶ℕ∞ ∧ {〈+∞, (ω × {1o})〉}:{+∞}⟶ℕ∞) ∧ (ℕ0 ∩ {+∞}) = ∅) → ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}):(ℕ0 ∪ {+∞})⟶ℕ∞) | |
25 | 17, 23, 24 | mp2an 424 | . . 3 ⊢ ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}):(ℕ0 ∪ {+∞})⟶ℕ∞ |
26 | fxnn0nninf.i | . . . 4 ⊢ 𝐼 = ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}) | |
27 | 26 | feq1i 5342 | . . 3 ⊢ (𝐼:(ℕ0 ∪ {+∞})⟶ℕ∞ ↔ ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}):(ℕ0 ∪ {+∞})⟶ℕ∞) |
28 | 25, 27 | mpbir 145 | . 2 ⊢ 𝐼:(ℕ0 ∪ {+∞})⟶ℕ∞ |
29 | df-xnn0 9203 | . . 3 ⊢ ℕ0* = (ℕ0 ∪ {+∞}) | |
30 | 29 | feq2i 5343 | . 2 ⊢ (𝐼:ℕ0*⟶ℕ∞ ↔ 𝐼:(ℕ0 ∪ {+∞})⟶ℕ∞) |
31 | 28, 30 | mpbir 145 | 1 ⊢ 𝐼:ℕ0*⟶ℕ∞ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 103 = wceq 1349 ∈ wcel 2142 ∪ cun 3120 ∩ cin 3121 ⊆ wss 3122 ∅c0 3415 ifcif 3527 {csn 3584 〈cop 3587 ↦ cmpt 4051 ωcom 4575 × cxp 4610 ◡ccnv 4611 ∘ ccom 4616 ⟶wf 5196 –1-1-onto→wf1o 5199 (class class class)co 5857 freccfrec 6373 1oc1o 6392 ℕ∞xnninf 7100 0cc0 7778 1c1 7779 + caddc 7781 +∞cpnf 7955 ℕ0cn0 9139 ℕ0*cxnn0 9202 ℤcz 9216 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-13 2144 ax-14 2145 ax-ext 2153 ax-coll 4105 ax-sep 4108 ax-nul 4116 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522 ax-iinf 4573 ax-cnex 7869 ax-resscn 7870 ax-1cn 7871 ax-1re 7872 ax-icn 7873 ax-addcl 7874 ax-addrcl 7875 ax-mulcl 7876 ax-addcom 7878 ax-addass 7880 ax-distr 7882 ax-i2m1 7883 ax-0lt1 7884 ax-0id 7886 ax-rnegex 7887 ax-cnre 7889 ax-pre-ltirr 7890 ax-pre-ltwlin 7891 ax-pre-lttrn 7892 ax-pre-ltadd 7894 |
This theorem depends on definitions: df-bi 116 df-dc 831 df-3or 975 df-3an 976 df-tru 1352 df-fal 1355 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ne 2342 df-nel 2437 df-ral 2454 df-rex 2455 df-reu 2456 df-rab 2458 df-v 2733 df-sbc 2957 df-csb 3051 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-nul 3416 df-if 3528 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-uni 3798 df-int 3833 df-iun 3876 df-br 3991 df-opab 4052 df-mpt 4053 df-tr 4089 df-id 4279 df-iord 4352 df-on 4354 df-ilim 4355 df-suc 4357 df-iom 4576 df-xp 4618 df-rel 4619 df-cnv 4620 df-co 4621 df-dm 4622 df-rn 4623 df-res 4624 df-ima 4625 df-iota 5162 df-fun 5202 df-fn 5203 df-f 5204 df-f1 5205 df-fo 5206 df-f1o 5207 df-fv 5208 df-riota 5813 df-ov 5860 df-oprab 5861 df-mpo 5862 df-recs 6288 df-frec 6374 df-1o 6399 df-2o 6400 df-map 6632 df-nninf 7101 df-pnf 7960 df-mnf 7961 df-xr 7962 df-ltxr 7963 df-le 7964 df-sub 8096 df-neg 8097 df-inn 8883 df-n0 9140 df-xnn0 9203 df-z 9217 df-uz 9492 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |