# Metamath Proof Explorer

## Theorem ordeleqon

Description: A way to express the ordinal property of a class in terms of the class of ordinal numbers. Corollary 7.14 of TakeutiZaring p. 38 and its converse. (Contributed by NM, 1-Jun-2003)

Ref Expression
Assertion ordeleqon ${⊢}\mathrm{Ord}{A}↔\left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)$

### Proof

Step Hyp Ref Expression
1 onprc ${⊢}¬\mathrm{On}\in \mathrm{V}$
2 elex ${⊢}\mathrm{On}\in {A}\to \mathrm{On}\in \mathrm{V}$
3 1 2 mto ${⊢}¬\mathrm{On}\in {A}$
4 ordon ${⊢}\mathrm{Ord}\mathrm{On}$
5 ordtri3or ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}\mathrm{On}\right)\to \left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\vee \mathrm{On}\in {A}\right)$
6 4 5 mpan2 ${⊢}\mathrm{Ord}{A}\to \left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\vee \mathrm{On}\in {A}\right)$
7 df-3or ${⊢}\left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\vee \mathrm{On}\in {A}\right)↔\left(\left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)\vee \mathrm{On}\in {A}\right)$
8 6 7 sylib ${⊢}\mathrm{Ord}{A}\to \left(\left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)\vee \mathrm{On}\in {A}\right)$
9 8 ord ${⊢}\mathrm{Ord}{A}\to \left(¬\left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)\to \mathrm{On}\in {A}\right)$
10 3 9 mt3i ${⊢}\mathrm{Ord}{A}\to \left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)$
11 eloni ${⊢}{A}\in \mathrm{On}\to \mathrm{Ord}{A}$
12 ordeq ${⊢}{A}=\mathrm{On}\to \left(\mathrm{Ord}{A}↔\mathrm{Ord}\mathrm{On}\right)$
13 4 12 mpbiri ${⊢}{A}=\mathrm{On}\to \mathrm{Ord}{A}$
14 11 13 jaoi ${⊢}\left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)\to \mathrm{Ord}{A}$
15 10 14 impbii ${⊢}\mathrm{Ord}{A}↔\left({A}\in \mathrm{On}\vee {A}=\mathrm{On}\right)$