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 7068 instead of infnninfOLD 7069. 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 7071. |
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 10340 | . . . . 5 ⊢ (𝐹 ∘ ◡𝐺):ℕ0⟶ℕ∞ |
4 | pnfex 7932 | . . . . . . . 8 ⊢ +∞ ∈ V | |
5 | omex 4553 | . . . . . . . . 9 ⊢ ω ∈ V | |
6 | 1oex 6372 | . . . . . . . . . 10 ⊢ 1o ∈ V | |
7 | 6 | snex 4147 | . . . . . . . . 9 ⊢ {1o} ∈ V |
8 | 5, 7 | xpex 4702 | . . . . . . . 8 ⊢ (ω × {1o}) ∈ V |
9 | 4, 8 | f1osn 5455 | . . . . . . 7 ⊢ {〈+∞, (ω × {1o})〉}:{+∞}–1-1-onto→{(ω × {1o})} |
10 | f1of 5415 | . . . . . . 7 ⊢ ({〈+∞, (ω × {1o})〉}:{+∞}–1-1-onto→{(ω × {1o})} → {〈+∞, (ω × {1o})〉}:{+∞}⟶{(ω × {1o})}) | |
11 | 9, 10 | ax-mp 5 | . . . . . 6 ⊢ {〈+∞, (ω × {1o})〉}:{+∞}⟶{(ω × {1o})} |
12 | infnninfOLD 7069 | . . . . . . 7 ⊢ (ω × {1o}) ∈ ℕ∞ | |
13 | snssi 3701 | . . . . . . 7 ⊢ ((ω × {1o}) ∈ ℕ∞ → {(ω × {1o})} ⊆ ℕ∞) | |
14 | 12, 13 | ax-mp 5 | . . . . . 6 ⊢ {(ω × {1o})} ⊆ ℕ∞ |
15 | fss 5332 | . . . . . 6 ⊢ (({〈+∞, (ω × {1o})〉}:{+∞}⟶{(ω × {1o})} ∧ {(ω × {1o})} ⊆ ℕ∞) → {〈+∞, (ω × {1o})〉}:{+∞}⟶ℕ∞) | |
16 | 11, 14, 15 | mp2an 423 | . . . . 5 ⊢ {〈+∞, (ω × {1o})〉}:{+∞}⟶ℕ∞ |
17 | 3, 16 | pm3.2i 270 | . . . 4 ⊢ ((𝐹 ∘ ◡𝐺):ℕ0⟶ℕ∞ ∧ {〈+∞, (ω × {1o})〉}:{+∞}⟶ℕ∞) |
18 | disj 3442 | . . . . 5 ⊢ ((ℕ0 ∩ {+∞}) = ∅ ↔ ∀𝑥 ∈ ℕ0 ¬ 𝑥 ∈ {+∞}) | |
19 | nn0nepnf 9162 | . . . . . . 7 ⊢ (𝑥 ∈ ℕ0 → 𝑥 ≠ +∞) | |
20 | 19 | neneqd 2348 | . . . . . 6 ⊢ (𝑥 ∈ ℕ0 → ¬ 𝑥 = +∞) |
21 | elsni 3578 | . . . . . 6 ⊢ (𝑥 ∈ {+∞} → 𝑥 = +∞) | |
22 | 20, 21 | nsyl 618 | . . . . 5 ⊢ (𝑥 ∈ ℕ0 → ¬ 𝑥 ∈ {+∞}) |
23 | 18, 22 | mprgbir 2515 | . . . 4 ⊢ (ℕ0 ∩ {+∞}) = ∅ |
24 | fun2 5344 | . . . 4 ⊢ ((((𝐹 ∘ ◡𝐺):ℕ0⟶ℕ∞ ∧ {〈+∞, (ω × {1o})〉}:{+∞}⟶ℕ∞) ∧ (ℕ0 ∩ {+∞}) = ∅) → ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}):(ℕ0 ∪ {+∞})⟶ℕ∞) | |
25 | 17, 23, 24 | mp2an 423 | . . 3 ⊢ ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}):(ℕ0 ∪ {+∞})⟶ℕ∞ |
26 | fxnn0nninf.i | . . . 4 ⊢ 𝐼 = ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}) | |
27 | 26 | feq1i 5313 | . . 3 ⊢ (𝐼:(ℕ0 ∪ {+∞})⟶ℕ∞ ↔ ((𝐹 ∘ ◡𝐺) ∪ {〈+∞, (ω × {1o})〉}):(ℕ0 ∪ {+∞})⟶ℕ∞) |
28 | 25, 27 | mpbir 145 | . 2 ⊢ 𝐼:(ℕ0 ∪ {+∞})⟶ℕ∞ |
29 | df-xnn0 9155 | . . 3 ⊢ ℕ0* = (ℕ0 ∪ {+∞}) | |
30 | 29 | feq2i 5314 | . 2 ⊢ (𝐼:ℕ0*⟶ℕ∞ ↔ 𝐼:(ℕ0 ∪ {+∞})⟶ℕ∞) |
31 | 28, 30 | mpbir 145 | 1 ⊢ 𝐼:ℕ0*⟶ℕ∞ |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∧ wa 103 = wceq 1335 ∈ wcel 2128 ∪ cun 3100 ∩ cin 3101 ⊆ wss 3102 ∅c0 3394 ifcif 3505 {csn 3560 〈cop 3563 ↦ cmpt 4026 ωcom 4550 × cxp 4585 ◡ccnv 4586 ∘ ccom 4591 ⟶wf 5167 –1-1-onto→wf1o 5170 (class class class)co 5825 freccfrec 6338 1oc1o 6357 ℕ∞xnninf 7064 0cc0 7733 1c1 7734 + caddc 7736 +∞cpnf 7910 ℕ0cn0 9091 ℕ0*cxnn0 9154 ℤcz 9168 |
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 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-coll 4080 ax-sep 4083 ax-nul 4091 ax-pow 4136 ax-pr 4170 ax-un 4394 ax-setind 4497 ax-iinf 4548 ax-cnex 7824 ax-resscn 7825 ax-1cn 7826 ax-1re 7827 ax-icn 7828 ax-addcl 7829 ax-addrcl 7830 ax-mulcl 7831 ax-addcom 7833 ax-addass 7835 ax-distr 7837 ax-i2m1 7838 ax-0lt1 7839 ax-0id 7841 ax-rnegex 7842 ax-cnre 7844 ax-pre-ltirr 7845 ax-pre-ltwlin 7846 ax-pre-lttrn 7847 ax-pre-ltadd 7849 |
This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-nel 2423 df-ral 2440 df-rex 2441 df-reu 2442 df-rab 2444 df-v 2714 df-sbc 2938 df-csb 3032 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3395 df-if 3506 df-pw 3545 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3774 df-int 3809 df-iun 3852 df-br 3967 df-opab 4027 df-mpt 4028 df-tr 4064 df-id 4254 df-iord 4327 df-on 4329 df-ilim 4330 df-suc 4332 df-iom 4551 df-xp 4593 df-rel 4594 df-cnv 4595 df-co 4596 df-dm 4597 df-rn 4598 df-res 4599 df-ima 4600 df-iota 5136 df-fun 5173 df-fn 5174 df-f 5175 df-f1 5176 df-fo 5177 df-f1o 5178 df-fv 5179 df-riota 5781 df-ov 5828 df-oprab 5829 df-mpo 5830 df-recs 6253 df-frec 6339 df-1o 6364 df-2o 6365 df-map 6596 df-nninf 7065 df-pnf 7915 df-mnf 7916 df-xr 7917 df-ltxr 7918 df-le 7919 df-sub 8049 df-neg 8050 df-inn 8835 df-n0 9092 df-xnn0 9155 df-z 9169 df-uz 9441 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |