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 5650 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Ord 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 1977 Ord word 5639 Oncon0 5640 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-v 3175 df-in 3547 df-ss 3554 df-uni 4373 df-tr 4681 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-ord 5643 df-on 5644 |
This theorem is referenced by: ontrci 5750 onirri 5751 onun2i 5760 onuniorsuci 6931 onsucssi 6933 oawordeulem 7521 omopthi 7624 bndrank 8587 rankprb 8597 rankuniss 8612 rankelun 8618 rankelpr 8619 rankelop 8620 rankmapu 8624 rankxplim3 8627 rankxpsuc 8628 cardlim 8681 carduni 8690 dfac8b 8737 alephdom2 8793 alephfp 8814 dfac12lem2 8849 pm110.643ALT 8883 cfsmolem 8975 ttukeylem6 9219 ttukeylem7 9220 unsnen 9254 mreexexdOLD 16132 efgmnvl 17950 nodenselem4 31083 hfuni 31461 finxpsuclem 32410 pwfi2f1o 36684 |
Copyright terms: Public domain | W3C validator |