Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nnnninf2 | GIF version |
Description: Canonical embedding of suc ω into ℕ∞. (Contributed by BJ, 10-Aug-2024.) |
Ref | Expression |
---|---|
nnnninf2 | ⊢ (𝑁 ∈ suc ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsuci 4389 | . 2 ⊢ (𝑁 ∈ suc ω → (𝑁 ∈ ω ∨ 𝑁 = ω)) | |
2 | nnnninf 7106 | . . 3 ⊢ (𝑁 ∈ ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) | |
3 | iftrue 3532 | . . . . . . 7 ⊢ (𝑖 ∈ ω → if(𝑖 ∈ ω, 1o, ∅) = 1o) | |
4 | 3 | eqcomd 2177 | . . . . . 6 ⊢ (𝑖 ∈ ω → 1o = if(𝑖 ∈ ω, 1o, ∅)) |
5 | eleq2 2235 | . . . . . . . 8 ⊢ (𝑁 = ω → (𝑖 ∈ 𝑁 ↔ 𝑖 ∈ ω)) | |
6 | 5 | ifbid 3548 | . . . . . . 7 ⊢ (𝑁 = ω → if(𝑖 ∈ 𝑁, 1o, ∅) = if(𝑖 ∈ ω, 1o, ∅)) |
7 | 6 | eqcomd 2177 | . . . . . 6 ⊢ (𝑁 = ω → if(𝑖 ∈ ω, 1o, ∅) = if(𝑖 ∈ 𝑁, 1o, ∅)) |
8 | 4, 7 | sylan9eqr 2226 | . . . . 5 ⊢ ((𝑁 = ω ∧ 𝑖 ∈ ω) → 1o = if(𝑖 ∈ 𝑁, 1o, ∅)) |
9 | 8 | mpteq2dva 4080 | . . . 4 ⊢ (𝑁 = ω → (𝑖 ∈ ω ↦ 1o) = (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅))) |
10 | infnninf 7104 | . . . 4 ⊢ (𝑖 ∈ ω ↦ 1o) ∈ ℕ∞ | |
11 | 9, 10 | eqeltrrdi 2263 | . . 3 ⊢ (𝑁 = ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) |
12 | 2, 11 | jaoi 712 | . 2 ⊢ ((𝑁 ∈ ω ∨ 𝑁 = ω) → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) |
13 | 1, 12 | syl 14 | 1 ⊢ (𝑁 ∈ suc ω → (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑁, 1o, ∅)) ∈ ℕ∞) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 704 = wceq 1349 ∈ wcel 2142 ∅c0 3415 ifcif 3527 ↦ cmpt 4051 suc csuc 4351 ωcom 4575 1oc1o 6392 ℕ∞xnninf 7100 |
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-sep 4108 ax-nul 4116 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522 ax-iinf 4573 |
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-ral 2454 df-rex 2455 df-rab 2458 df-v 2733 df-sbc 2957 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-br 3991 df-opab 4052 df-mpt 4053 df-tr 4089 df-id 4279 df-iord 4352 df-on 4354 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-fv 5208 df-ov 5860 df-oprab 5861 df-mpo 5862 df-1o 6399 df-2o 6400 df-map 6632 df-nninf 7101 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |