# Metamath Proof Explorer

## Theorem ordom

Description: Omega 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 dftr2 ${⊢}\mathrm{Tr}\mathrm{\omega }↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {x}\wedge {x}\in \mathrm{\omega }\right)\to {y}\in \mathrm{\omega }\right)$
2 onelon ${⊢}\left({x}\in \mathrm{On}\wedge {y}\in {x}\right)\to {y}\in \mathrm{On}$
3 2 expcom ${⊢}{y}\in {x}\to \left({x}\in \mathrm{On}\to {y}\in \mathrm{On}\right)$
4 limord ${⊢}\mathrm{Lim}{z}\to \mathrm{Ord}{z}$
5 ordtr ${⊢}\mathrm{Ord}{z}\to \mathrm{Tr}{z}$
6 trel ${⊢}\mathrm{Tr}{z}\to \left(\left({y}\in {x}\wedge {x}\in {z}\right)\to {y}\in {z}\right)$
7 4 5 6 3syl ${⊢}\mathrm{Lim}{z}\to \left(\left({y}\in {x}\wedge {x}\in {z}\right)\to {y}\in {z}\right)$
8 7 expd ${⊢}\mathrm{Lim}{z}\to \left({y}\in {x}\to \left({x}\in {z}\to {y}\in {z}\right)\right)$
9 8 com12 ${⊢}{y}\in {x}\to \left(\mathrm{Lim}{z}\to \left({x}\in {z}\to {y}\in {z}\right)\right)$
10 9 a2d ${⊢}{y}\in {x}\to \left(\left(\mathrm{Lim}{z}\to {x}\in {z}\right)\to \left(\mathrm{Lim}{z}\to {y}\in {z}\right)\right)$
11 10 alimdv ${⊢}{y}\in {x}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{z}\to {x}\in {z}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{z}\to {y}\in {z}\right)\right)$
12 3 11 anim12d ${⊢}{y}\in {x}\to \left(\left({x}\in \mathrm{On}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{z}\to {x}\in {z}\right)\right)\to \left({y}\in \mathrm{On}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{z}\to {y}\in {z}\right)\right)\right)$
13 elom ${⊢}{x}\in \mathrm{\omega }↔\left({x}\in \mathrm{On}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{z}\to {x}\in {z}\right)\right)$
14 elom ${⊢}{y}\in \mathrm{\omega }↔\left({y}\in \mathrm{On}\wedge \forall {z}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{z}\to {y}\in {z}\right)\right)$
15 12 13 14 3imtr4g ${⊢}{y}\in {x}\to \left({x}\in \mathrm{\omega }\to {y}\in \mathrm{\omega }\right)$
16 15 imp ${⊢}\left({y}\in {x}\wedge {x}\in \mathrm{\omega }\right)\to {y}\in \mathrm{\omega }$
17 16 ax-gen ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({y}\in {x}\wedge {x}\in \mathrm{\omega }\right)\to {y}\in \mathrm{\omega }\right)$
18 1 17 mpgbir ${⊢}\mathrm{Tr}\mathrm{\omega }$
19 omsson ${⊢}\mathrm{\omega }\subseteq \mathrm{On}$
20 ordon ${⊢}\mathrm{Ord}\mathrm{On}$
21 trssord ${⊢}\left(\mathrm{Tr}\mathrm{\omega }\wedge \mathrm{\omega }\subseteq \mathrm{On}\wedge \mathrm{Ord}\mathrm{On}\right)\to \mathrm{Ord}\mathrm{\omega }$
22 18 19 20 21 mp3an ${⊢}\mathrm{Ord}\mathrm{\omega }$