![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2onn | Structured version Visualization version GIF version |
Description: The ordinal 2 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un 7725, see 2onnALT 8642. (Contributed by NM, 28-Sep-2004.) Avoid ax-un 7725. (Revised by BTernaryTau, 1-Dec-2024.) |
Ref | Expression |
---|---|
2onn | ⊢ 2o ∈ ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2on 8480 | . 2 ⊢ 2o ∈ On | |
2 | 2ellim 8499 | . . 3 ⊢ (Lim 𝑥 → 2o ∈ 𝑥) | |
3 | 2 | ax-gen 1798 | . 2 ⊢ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥) |
4 | elom 7858 | . 2 ⊢ (2o ∈ ω ↔ (2o ∈ On ∧ ∀𝑥(Lim 𝑥 → 2o ∈ 𝑥))) | |
5 | 1, 3, 4 | mpbir2an 710 | 1 ⊢ 2o ∈ ω |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1540 ∈ wcel 2107 Oncon0 6365 Lim wlim 6366 ωcom 7855 2oc2o 8460 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-tr 5267 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-om 7856 df-1o 8466 df-2o 8467 |
This theorem is referenced by: 3onn 8643 nn2m 8653 nnneo 8654 nneob 8655 omopthlem1 8658 omopthlem2 8659 pwen 9150 en2eqpr 10002 en2eleq 10003 unctb 10200 infdjuabs 10201 ackbij1lem5 10219 sdom2en01 10297 fin56 10388 fin67 10390 fin1a2lem4 10398 alephexp1 10574 pwcfsdom 10578 alephom 10580 canthp1lem2 10648 pwxpndom2 10660 hash3 14366 hash2pr 14430 pr2pwpr 14440 rpnnen 16170 rexpen 16171 xpsfrnel 17508 xpscf 17511 symggen 19338 psgnunilem1 19361 simpgnsgd 19970 znfld 21116 hauspwdom 23005 xpsmet 23888 xpsxms 24043 xpsms 24044 unidifsnel 31772 unidifsnne 31773 sat1el2xp 34370 ex-sategoelelomsuc 34417 ex-sategoelel12 34418 1oequni2o 36249 finxpreclem4 36275 finxp3o 36281 wepwso 41785 frlmpwfi 41840 2omomeqom 42053 oenord1ex 42065 oaomoencom 42067 2finon 42201 har2o 42297 |
Copyright terms: Public domain | W3C validator |