| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 1onn | Structured version Visualization version GIF version | ||
| Description: The ordinal 1 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7755, see 1onnALT 8679. Lemma 2.2 of [Schloeder] p. 4. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7755. (Revised by BTernaryTau, 1-Dec-2024.) |
| Ref | Expression |
|---|---|
| 1onn | ⊢ 1o ∈ ω |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1on 8518 | . 2 ⊢ 1o ∈ On | |
| 2 | 1ellim 8536 | . . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥) | |
| 3 | 2 | ax-gen 1795 | . 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥) |
| 4 | elom 7890 | . 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥))) | |
| 5 | 1, 3, 4 | mpbir2an 711 | 1 ⊢ 1o ∈ ω |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∀wal 1538 ∈ wcel 2108 Oncon0 6384 Lim wlim 6385 ωcom 7887 1oc1o 8499 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-tr 5260 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-om 7888 df-1o 8506 |
| This theorem is referenced by: 2onnALT 8681 1one2o 8684 oaabs2 8687 omabs 8689 nnm2 8691 nnneo 8693 nneob 8694 snfi 9083 snfiOLD 9084 snnen2oOLD 9264 1sdom2ALT 9277 1sdomOLD 9285 unxpdom2 9290 en1eqsnOLD 9309 wofib 9585 oancom 9691 cnfcom3clem 9745 ssttrcl 9755 ttrcltr 9756 djurf1o 9953 card1 10008 pm54.43lem 10040 en2eleq 10048 en2other2 10049 infxpenlem 10053 infxpenc2lem1 10059 sdom2en01 10342 cfpwsdom 10624 canthp1lem2 10693 gchdju1 10696 pwxpndom2 10705 pwdjundom 10707 1pi 10923 1lt2pi 10945 indpi 10947 hash2 14444 hash1snb 14458 fnpr2o 17602 fvpr1o 17605 f1otrspeq 19465 pmtrf 19473 pmtrmvd 19474 pmtrfinv 19479 lt6abl 19913 isnzr2 20518 frgpcyg 21592 vr1cl 22219 ply1coe 22302 isppw 27157 pw2bday 28418 bnj906 34944 sat1el2xp 35384 satfv1fvfmla1 35428 satefvfmla1 35430 ex-sategoelelomsuc 35431 ex-sategoelel12 35432 finxpreclem1 37390 finxpreclem2 37391 finxp1o 37393 finxpreclem4 37395 finxp2o 37400 domalom 37405 onexoegt 43256 1oaomeqom 43306 oaabsb 43307 omnord1ex 43317 oaomoencom 43330 cantnftermord 43333 cantnf2 43338 omabs2 43345 omcl2 43346 1finon 43462 finona1cl 43466 1iscard 43555 |
| Copyright terms: Public domain | W3C validator |