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	$⊢ Ord A \leftrightarrow (A \in On \lor A = On)$

Proof

Step	Hyp	Ref	Expression
1		onprc	$⊢ \neg On \in V$
2		elex	$⊢ On \in A \to On \in V$
3	1 2	mto	$⊢ \neg On \in A$
4		ordon	$⊢ Ord On$
5		ordtri3or	$⊢ (Ord A \land Ord On) \to (A \in On \lor A = On \lor On \in A)$
6	4 5	mpan2	$⊢ Ord A \to (A \in On \lor A = On \lor On \in A)$
7		df-3or	$⊢ (A \in On \lor A = On \lor On \in A) \leftrightarrow ((A \in On \lor A = On) \lor On \in A)$
8	6 7	sylib	$⊢ Ord A \to ((A \in On \lor A = On) \lor On \in A)$
9	8	ord	$⊢ Ord A \to (\neg (A \in On \lor A = On) \to On \in A)$
10	3 9	mt3i	$⊢ Ord A \to (A \in On \lor A = On)$
11		eloni	$⊢ A \in On \to Ord A$
12		ordeq	$⊢ A = On \to (Ord A \leftrightarrow Ord On)$
13	4 12	mpbiri	$⊢ A = On \to Ord A$
14	11 13	jaoi	$⊢ (A \in On \lor A = On) \to Ord A$
15	10 14	impbii	$⊢ Ord A \leftrightarrow (A \in On \lor A = On)$