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	$$⊢\mathrm{Ord}\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		trom	$$⊢\mathrm{Tr}\mathrm{\omega }$$
2		omsson	$$⊢\mathrm{\omega }\subseteq \mathrm{On}$$
3		ordon	$$⊢\mathrm{Ord}\mathrm{On}$$
4		trssord	$$⊢\left(\mathrm{Tr}\mathrm{\omega }\wedge \mathrm{\omega }\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{On}\right)\to \mathrm{Ord}\mathrm{\omega }$$
5	1 2 3 4	mp3an	$$⊢\mathrm{Ord}\mathrm{\omega }$$