| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > infnninf | GIF version | ||
| Description: The point at infinity in ℕ∞ is the constant sequence equal to 1o. Note that with our encoding of functions, that constant function can also be expressed as (ω × {1o}), as fconstmpt 4773 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.) |
| Ref | Expression |
|---|---|
| infnninf | ⊢ (𝑖 ∈ ω ↦ 1o) ∈ ℕ∞ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1lt2o 6610 | . . . . . 6 ⊢ 1o ∈ 2o | |
| 2 | 1 | a1i 9 | . . . . 5 ⊢ ((⊤ ∧ 𝑖 ∈ ω) → 1o ∈ 2o) |
| 3 | 2 | fmpttd 5802 | . . . 4 ⊢ (⊤ → (𝑖 ∈ ω ↦ 1o):ω⟶2o) |
| 4 | 3 | mptru 1406 | . . 3 ⊢ (𝑖 ∈ ω ↦ 1o):ω⟶2o |
| 5 | 2on 6591 | . . . 4 ⊢ 2o ∈ On | |
| 6 | omex 4691 | . . . 4 ⊢ ω ∈ V | |
| 7 | elmapg 6830 | . . . 4 ⊢ ((2o ∈ On ∧ ω ∈ V) → ((𝑖 ∈ ω ↦ 1o) ∈ (2o ↑𝑚 ω) ↔ (𝑖 ∈ ω ↦ 1o):ω⟶2o)) | |
| 8 | 5, 6, 7 | mp2an 426 | . . 3 ⊢ ((𝑖 ∈ ω ↦ 1o) ∈ (2o ↑𝑚 ω) ↔ (𝑖 ∈ ω ↦ 1o):ω⟶2o) |
| 9 | 4, 8 | mpbir 146 | . 2 ⊢ (𝑖 ∈ ω ↦ 1o) ∈ (2o ↑𝑚 ω) |
| 10 | peano2 4693 | . . . . . 6 ⊢ (𝑗 ∈ ω → suc 𝑗 ∈ ω) | |
| 11 | eqidd 2232 | . . . . . . 7 ⊢ (𝑖 = suc 𝑗 → 1o = 1o) | |
| 12 | eqid 2231 | . . . . . . 7 ⊢ (𝑖 ∈ ω ↦ 1o) = (𝑖 ∈ ω ↦ 1o) | |
| 13 | 1oex 6590 | . . . . . . 7 ⊢ 1o ∈ V | |
| 14 | 11, 12, 13 | fvmpt 5723 | . . . . . 6 ⊢ (suc 𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) = 1o) |
| 15 | 10, 14 | syl 14 | . . . . 5 ⊢ (𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) = 1o) |
| 16 | eqidd 2232 | . . . . . 6 ⊢ (𝑖 = 𝑗 → 1o = 1o) | |
| 17 | 16, 12, 13 | fvmpt 5723 | . . . . 5 ⊢ (𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘𝑗) = 1o) |
| 18 | 15, 17 | eqtr4d 2267 | . . . 4 ⊢ (𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) = ((𝑖 ∈ ω ↦ 1o)‘𝑗)) |
| 19 | eqimss 3281 | . . . 4 ⊢ (((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) = ((𝑖 ∈ ω ↦ 1o)‘𝑗) → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗)) | |
| 20 | 18, 19 | syl 14 | . . 3 ⊢ (𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗)) |
| 21 | 20 | rgen 2585 | . 2 ⊢ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗) |
| 22 | fveq1 5638 | . . . . 5 ⊢ (𝑓 = (𝑖 ∈ ω ↦ 1o) → (𝑓‘suc 𝑗) = ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗)) | |
| 23 | fveq1 5638 | . . . . 5 ⊢ (𝑓 = (𝑖 ∈ ω ↦ 1o) → (𝑓‘𝑗) = ((𝑖 ∈ ω ↦ 1o)‘𝑗)) | |
| 24 | 22, 23 | sseq12d 3258 | . . . 4 ⊢ (𝑓 = (𝑖 ∈ ω ↦ 1o) → ((𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗))) |
| 25 | 24 | ralbidv 2532 | . . 3 ⊢ (𝑓 = (𝑖 ∈ ω ↦ 1o) → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗) ↔ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗))) |
| 26 | df-nninf 7319 | . . 3 ⊢ ℕ∞ = {𝑓 ∈ (2o ↑𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓‘𝑗)} | |
| 27 | 25, 26 | elrab2 2965 | . 2 ⊢ ((𝑖 ∈ ω ↦ 1o) ∈ ℕ∞ ↔ ((𝑖 ∈ ω ↦ 1o) ∈ (2o ↑𝑚 ω) ∧ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗))) |
| 28 | 9, 21, 27 | mpbir2an 950 | 1 ⊢ (𝑖 ∈ ω ↦ 1o) ∈ ℕ∞ |
| Colors of variables: wff set class |
| Syntax hints: ∧ wa 104 ↔ wb 105 = wceq 1397 ⊤wtru 1398 ∈ wcel 2202 ∀wral 2510 Vcvv 2802 ⊆ wss 3200 ↦ cmpt 4150 Oncon0 4460 suc csuc 4462 ωcom 4688 ⟶wf 5322 ‘cfv 5326 (class class class)co 6018 1oc1o 6575 2oc2o 6576 ↑𝑚 cmap 6817 ℕ∞xnninf 7318 |
| 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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530 ax-setind 4635 ax-iinf 4686 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-ral 2515 df-rex 2516 df-rab 2519 df-v 2804 df-sbc 3032 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-int 3929 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-iord 4463 df-on 4465 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-res 4737 df-ima 4738 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-fv 5334 df-ov 6021 df-oprab 6022 df-mpo 6023 df-1o 6582 df-2o 6583 df-map 6819 df-nninf 7319 |
| This theorem is referenced by: nnnninf2 7326 nninfwlpoimlemdc 7376 nninfct 12614 nninffeq 16643 nnnninfen 16644 |
| Copyright terms: Public domain | W3C validator |