Theorem ordom

Description: The class of finite ordinals _om is ordinal. Theorem 7.32 of TakeutiZaring p. 43. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	ordom	⊢ Ord ω

Proof

Step	Hyp	Ref	Expression
1		trom	⊢ Tr ω
2		omsson	⊢ ω ⊆ On
3		ordon	⊢ Ord On
4		trssord	⊢ ( ( Tr ω ∧ ω ⊆ On ∧ Ord On ) → Ord ω )
5	1 2 3 4	mp3an	⊢ Ord ω