Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  infnninf GIF version

Theorem infnninf 7056
 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 4630 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
Assertion
Ref Expression
infnninf (𝑖 ∈ ω ↦ 1o) ∈ ℕ

Proof of Theorem infnninf
Dummy variables 𝑓 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1lt2o 6383 . . . . . 6 1o ∈ 2o
21a1i 9 . . . . 5 ((⊤ ∧ 𝑖 ∈ ω) → 1o ∈ 2o)
32fmpttd 5619 . . . 4 (⊤ → (𝑖 ∈ ω ↦ 1o):ω⟶2o)
43mptru 1344 . . 3 (𝑖 ∈ ω ↦ 1o):ω⟶2o
5 2on 6366 . . . 4 2o ∈ On
6 omex 4550 . . . 4 ω ∈ V
7 elmapg 6599 . . . 4 ((2o ∈ On ∧ ω ∈ V) → ((𝑖 ∈ ω ↦ 1o) ∈ (2o𝑚 ω) ↔ (𝑖 ∈ ω ↦ 1o):ω⟶2o))
85, 6, 7mp2an 423 . . 3 ((𝑖 ∈ ω ↦ 1o) ∈ (2o𝑚 ω) ↔ (𝑖 ∈ ω ↦ 1o):ω⟶2o)
94, 8mpbir 145 . 2 (𝑖 ∈ ω ↦ 1o) ∈ (2o𝑚 ω)
10 peano2 4552 . . . . . 6 (𝑗 ∈ ω → suc 𝑗 ∈ ω)
11 eqidd 2158 . . . . . . 7 (𝑖 = suc 𝑗 → 1o = 1o)
12 eqid 2157 . . . . . . 7 (𝑖 ∈ ω ↦ 1o) = (𝑖 ∈ ω ↦ 1o)
13 1oex 6365 . . . . . . 7 1o ∈ V
1411, 12, 13fvmpt 5542 . . . . . 6 (suc 𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) = 1o)
1510, 14syl 14 . . . . 5 (𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) = 1o)
16 eqidd 2158 . . . . . 6 (𝑖 = 𝑗 → 1o = 1o)
1716, 12, 13fvmpt 5542 . . . . 5 (𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘𝑗) = 1o)
1815, 17eqtr4d 2193 . . . 4 (𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) = ((𝑖 ∈ ω ↦ 1o)‘𝑗))
19 eqimss 3182 . . . 4 (((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) = ((𝑖 ∈ ω ↦ 1o)‘𝑗) → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗))
2018, 19syl 14 . . 3 (𝑗 ∈ ω → ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗))
2120rgen 2510 . 2 𝑗 ∈ ω ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗)
22 fveq1 5464 . . . . 5 (𝑓 = (𝑖 ∈ ω ↦ 1o) → (𝑓‘suc 𝑗) = ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗))
23 fveq1 5464 . . . . 5 (𝑓 = (𝑖 ∈ ω ↦ 1o) → (𝑓𝑗) = ((𝑖 ∈ ω ↦ 1o)‘𝑗))
2422, 23sseq12d 3159 . . . 4 (𝑓 = (𝑖 ∈ ω ↦ 1o) → ((𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗)))
2524ralbidv 2457 . . 3 (𝑓 = (𝑖 ∈ ω ↦ 1o) → (∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗) ↔ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗)))
26 df-nninf 7054 . . 3 = {𝑓 ∈ (2o𝑚 ω) ∣ ∀𝑗 ∈ ω (𝑓‘suc 𝑗) ⊆ (𝑓𝑗)}
2725, 26elrab2 2871 . 2 ((𝑖 ∈ ω ↦ 1o) ∈ ℕ ↔ ((𝑖 ∈ ω ↦ 1o) ∈ (2o𝑚 ω) ∧ ∀𝑗 ∈ ω ((𝑖 ∈ ω ↦ 1o)‘suc 𝑗) ⊆ ((𝑖 ∈ ω ↦ 1o)‘𝑗)))
289, 21, 27mpbir2an 927 1 (𝑖 ∈ ω ↦ 1o) ∈ ℕ
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1335  ⊤wtru 1336   ∈ wcel 2128  ∀wral 2435  Vcvv 2712   ⊆ wss 3102   ↦ cmpt 4025  Oncon0 4322  suc csuc 4324  ωcom 4547  ⟶wf 5163  ‘cfv 5167  (class class class)co 5818  1oc1o 6350  2oc2o 6351   ↑𝑚 cmap 6586  ℕ∞xnninf 7053 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-sep 4082  ax-nul 4090  ax-pow 4134  ax-pr 4168  ax-un 4392  ax-setind 4494  ax-iinf 4545 This theorem depends on definitions:  df-bi 116  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-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-id 4252  df-iord 4325  df-on 4327  df-suc 4330  df-iom 4548  df-xp 4589  df-rel 4590  df-cnv 4591  df-co 4592  df-dm 4593  df-rn 4594  df-res 4595  df-ima 4596  df-iota 5132  df-fun 5169  df-fn 5170  df-f 5171  df-fv 5175  df-ov 5821  df-oprab 5822  df-mpo 5823  df-1o 6357  df-2o 6358  df-map 6588  df-nninf 7054 This theorem is referenced by:  nnnninf2  7059  nninffeq  13555
 Copyright terms: Public domain W3C validator