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	|- ( Ord A <-> ( A e. On \/ A = On ) )

Proof

Step	Hyp	Ref	Expression
1		onprc	|- -. On e. _V
2		elex	|- ( On e. A -> On e. _V )
3	1 2	mto	|- -. On e. A
4		ordon	|- Ord On
5		ordtri3or	|- ( ( Ord A /\ Ord On ) -> ( A e. On \/ A = On \/ On e. A ) )
6	4 5	mpan2	|- ( Ord A -> ( A e. On \/ A = On \/ On e. A ) )
7		df-3or	|- ( ( A e. On \/ A = On \/ On e. A ) <-> ( ( A e. On \/ A = On ) \/ On e. A ) )
8	6 7	sylib	|- ( Ord A -> ( ( A e. On \/ A = On ) \/ On e. A ) )
9	8	ord	|- ( Ord A -> ( -. ( A e. On \/ A = On ) -> On e. A ) )
10	3 9	mt3i	|- ( Ord A -> ( A e. On \/ A = On ) )
11		eloni	|- ( A e. On -> Ord A )
12		ordeq	|- ( A = On -> ( Ord A <-> Ord On ) )
13	4 12	mpbiri	|- ( A = On -> Ord A )
14	11 13	jaoi	|- ( ( A e. On \/ A = On ) -> Ord A )
15	10 14	impbii	|- ( Ord A <-> ( A e. On \/ A = On ) )