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

Theorem infnninf 7023
 Description: The point at infinity in ℕ∞ is the constant sequence equal to . Note that with our encoding of functions, that constant function can also be written as , as fconstmpt 4598 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)
Assertion
Ref Expression
infnninf

Proof of Theorem infnninf
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1lt2o 6351 . . . . . 6
21a1i 9 . . . . 5
32fmpttd 5587 . . . 4
43mptru 1341 . . 3
5 2on 6334 . . . 4
6 omex 4518 . . . 4
7 elmapg 6567 . . . 4
85, 6, 7mp2an 423 . . 3
94, 8mpbir 145 . 2
10 peano2 4520 . . . . . 6
11 eqidd 2142 . . . . . . 7
12 eqid 2141 . . . . . . 7
13 1oex 6333 . . . . . . 7
1411, 12, 13fvmpt 5510 . . . . . 6
1510, 14syl 14 . . . . 5
16 eqidd 2142 . . . . . 6
1716, 12, 13fvmpt 5510 . . . . 5
1815, 17eqtr4d 2177 . . . 4
19 eqimss 3158 . . . 4
2018, 19syl 14 . . 3
2120rgen 2490 . 2
22 fveq1 5432 . . . . 5
23 fveq1 5432 . . . . 5
2422, 23sseq12d 3135 . . . 4
2524ralbidv 2440 . . 3
26 df-nninf 7022 . . 3
2725, 26elrab2 2849 . 2
289, 21, 27mpbir2an 927 1
 Colors of variables: wff set class Syntax hints:   wa 103   wb 104   wceq 1332   wtru 1333   wcel 2112  wral 2418  cvv 2691   wss 3078   cmpt 3999  con0 4296   csuc 4298  com 4515  wf 5131  cfv 5135  (class class class)co 5786  c1o 6318  c2o 6319   cmap 6554  ℕ∞xnninf 7021 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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2114  ax-14 2115  ax-ext 2123  ax-sep 4056  ax-nul 4064  ax-pow 4108  ax-pr 4142  ax-un 4366  ax-setind 4463  ax-iinf 4513 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1732  df-eu 1993  df-mo 1994  df-clab 2128  df-cleq 2134  df-clel 2137  df-nfc 2272  df-ne 2311  df-ral 2423  df-rex 2424  df-rab 2427  df-v 2693  df-sbc 2916  df-dif 3080  df-un 3082  df-in 3084  df-ss 3091  df-nul 3371  df-pw 3519  df-sn 3540  df-pr 3541  df-op 3543  df-uni 3747  df-int 3782  df-br 3940  df-opab 4000  df-mpt 4001  df-tr 4037  df-id 4226  df-iord 4299  df-on 4301  df-suc 4304  df-iom 4516  df-xp 4557  df-rel 4558  df-cnv 4559  df-co 4560  df-dm 4561  df-rn 4562  df-res 4563  df-ima 4564  df-iota 5100  df-fun 5137  df-fn 5138  df-f 5139  df-fv 5143  df-ov 5789  df-oprab 5790  df-mpo 5791  df-1o 6325  df-2o 6326  df-map 6556  df-nninf 7022 This theorem is referenced by:  nnnninf2  7026  nninffeq  13435
 Copyright terms: Public domain W3C validator