![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > onordi | Structured version Visualization version GIF version |
Description: An ordinal number is an ordinal class. (Contributed by NM, 11-Jun-1994.) |
Ref | Expression |
---|---|
on.1 | ⊢ 𝐴 ∈ On |
Ref | Expression |
---|---|
onordi | ⊢ Ord 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | on.1 | . 2 ⊢ 𝐴 ∈ On | |
2 | eloni 6373 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Ord 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 Ord word 6362 Oncon0 6363 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3057 df-v 3471 df-in 3951 df-ss 3961 df-uni 4904 df-tr 5260 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-ord 6366 df-on 6367 |
This theorem is referenced by: onirri 6476 onsucssi 7839 ord1eln01 8510 ord2eln012 8511 oawordeulem 8568 omopthi 8675 en2 9297 en3 9298 ssttrcl 9730 ttrcltr 9731 dmttrcl 9736 ttrclselem2 9741 bndrank 9856 rankprb 9866 rankuniss 9881 rankelun 9887 rankelpr 9888 rankelop 9889 rankmapu 9893 rankxplim3 9896 rankxpsuc 9897 cardlim 9987 carduni 9996 dfac8b 10046 alephdom2 10102 alephfp 10123 dfac12lem2 10159 dju1p1e2ALT 10189 cfsmolem 10285 ttukeylem6 10529 ttukeylem7 10530 unsnen 10568 efgmnvl 19660 nogt01o 27616 scutbdaybnd2lim 27737 slerec 27739 bday1s 27751 cuteq1 27753 newbday 27815 negsproplem7 27933 mulsproplem13 28015 mulsproplem14 28016 sltonold 28140 hfuni 35716 finxpsuclem 36812 pwfi2f1o 42442 |
Copyright terms: Public domain | W3C validator |