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 𝐴 → 𝐴 ⊆ On )

Proof

Step	Hyp	Ref	Expression
1		ordon	⊢ Ord On
2		ordeleqon	⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
3	2	birani	⊢ ( ( Ord 𝐴 ∧ Ord On ) → ( 𝐴 ∈ On ∨ 𝐴 = On ) )
4		ordsseleq	⊢ ( ( Ord 𝐴 ∧ Ord On ) → ( 𝐴 ⊆ On ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) ) )
5	3 4	mpbird	⊢ ( ( Ord 𝐴 ∧ Ord On ) → 𝐴 ⊆ On )
6	1 5	mpan2	⊢ ( Ord 𝐴 → 𝐴 ⊆ On )