![]() |
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 7741, see 1onnALT 8662. Lemma 2.2 of [Schloeder] p. 4. (Contributed by NM, 29-Oct-1995.) Avoid ax-un 7741. (Revised by BTernaryTau, 1-Dec-2024.) |
Ref | Expression |
---|---|
1onn | ⊢ 1o ∈ ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1on 8499 | . 2 ⊢ 1o ∈ On | |
2 | 1ellim 8519 | . . 3 ⊢ (Lim 𝑥 → 1o ∈ 𝑥) | |
3 | 2 | ax-gen 1789 | . 2 ⊢ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥) |
4 | elom 7874 | . 2 ⊢ (1o ∈ ω ↔ (1o ∈ On ∧ ∀𝑥(Lim 𝑥 → 1o ∈ 𝑥))) | |
5 | 1, 3, 4 | mpbir2an 709 | 1 ⊢ 1o ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1531 ∈ wcel 2098 Oncon0 6371 Lim wlim 6372 ωcom 7871 1oc1o 8480 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-tr 5267 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-ord 6374 df-on 6375 df-lim 6376 df-suc 6377 df-om 7872 df-1o 8487 |
This theorem is referenced by: 2onnALT 8664 1one2o 8667 oaabs2 8670 omabs 8672 nnm2 8674 nnneo 8676 nneob 8677 snfi 9069 snnen2oOLD 9252 1sdom2ALT 9266 1sdomOLD 9274 unxpdom2 9279 en1eqsnOLD 9300 pwfiOLD 9373 wofib 9570 oancom 9676 cnfcom3clem 9730 ssttrcl 9740 ttrcltr 9741 djurf1o 9938 card1 9993 pm54.43lem 10025 en2eleq 10033 en2other2 10034 infxpenlem 10038 infxpenc2lem1 10044 sdom2en01 10327 cfpwsdom 10609 canthp1lem2 10678 gchdju1 10681 pwxpndom2 10690 pwdjundom 10692 1pi 10908 1lt2pi 10930 indpi 10932 hash2 14400 hash1snb 14414 fnpr2o 17542 fvpr1o 17545 f1otrspeq 19414 pmtrf 19422 pmtrmvd 19423 pmtrfinv 19428 lt6abl 19862 isnzr2 20469 frgpcyg 21524 vr1cl 22160 ply1coe 22242 isppw 27091 bnj906 34689 sat1el2xp 35117 satfv1fvfmla1 35161 satefvfmla1 35163 ex-sategoelelomsuc 35164 ex-sategoelel12 35165 finxpreclem1 36996 finxpreclem2 36997 finxp1o 36999 finxpreclem4 37001 finxp2o 37006 domalom 37011 onexoegt 42811 1oaomeqom 42861 oaabsb 42862 omnord1ex 42872 oaomoencom 42885 cantnftermord 42888 cantnf2 42893 omabs2 42900 omcl2 42901 1finon 43018 finona1cl 43022 1iscard 43111 |
Copyright terms: Public domain | W3C validator |