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	biimpi	⊢ ( Ord 𝐴 → ( 𝐴 ∈ On ∨ 𝐴 = On ) )
4	3	adantr	⊢ ( ( Ord 𝐴 ∧ Ord On ) → ( 𝐴 ∈ On ∨ 𝐴 = On ) )
5		ordsseleq	⊢ ( ( Ord 𝐴 ∧ Ord On ) → ( 𝐴 ⊆ On ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) ) )
6	4 5	mpbird	⊢ ( ( Ord 𝐴 ∧ Ord On ) → 𝐴 ⊆ On )
7	1 6	mpan2	⊢ ( Ord 𝐴 → 𝐴 ⊆ On )