![]() |
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 5951 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Ord 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 Ord word 5940 Oncon0 5941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-v 3387 df-in 3776 df-ss 3783 df-uni 4629 df-tr 4946 df-po 5233 df-so 5234 df-fr 5271 df-we 5273 df-ord 5944 df-on 5945 |
This theorem is referenced by: ontrci 6046 onirri 6047 onun2i 6056 onuniorsuci 7273 onsucssi 7275 oawordeulem 7874 omopthi 7977 bndrank 8954 rankprb 8964 rankuniss 8979 rankelun 8985 rankelpr 8986 rankelop 8987 rankmapu 8991 rankxplim3 8994 rankxpsuc 8995 cardlim 9084 carduni 9093 dfac8b 9140 alephdom2 9196 alephfp 9217 dfac12lem2 9254 pm110.643ALT 9288 cfsmolem 9380 ttukeylem6 9624 ttukeylem7 9625 unsnen 9663 efgmnvl 18440 slerec 32436 hfuni 32804 finxpsuclem 33732 pwfi2f1o 38451 |
Copyright terms: Public domain | W3C validator |