Metamath Proof Explorer

Theorem ordsson

Description: Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of TakeutiZaring p. 38. (Contributed by NM, 18-May-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011)

		Ref	Expression
	Assertion	ordsson	$⊢ Ord A \to A \subseteq On$

Proof

Step	Hyp	Ref	Expression
1		ordon	$⊢ Ord On$
2		ordeleqon	$⊢ Ord A \leftrightarrow (A \in On \lor A = On)$
3	2	biimpi	$⊢ Ord A \to (A \in On \lor A = On)$
4	3	adantr	$⊢ (Ord A \land Ord On) \to (A \in On \lor A = On)$
5		ordsseleq	$⊢ (Ord A \land Ord On) \to (A \subseteq On \leftrightarrow (A \in On \lor A = On))$
6	4 5	mpbird	$⊢ (Ord A \land Ord On) \to A \subseteq On$
7	1 6	mpan2	$⊢ Ord A \to A \subseteq On$