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	|- Ord _om

Proof

Step	Hyp	Ref	Expression
1		dftr2	|- ( Tr _om <-> A. y A. x ( ( y e. x /\ x e. _om ) -> y e. _om ) )
2		onelon	|- ( ( x e. On /\ y e. x ) -> y e. On )
3	2	expcom	|- ( y e. x -> ( x e. On -> y e. On ) )
4		limord	|- ( Lim z -> Ord z )
5		ordtr	|- ( Ord z -> Tr z )
6		trel	|- ( Tr z -> ( ( y e. x /\ x e. z ) -> y e. z ) )
7	4 5 6	3syl	|- ( Lim z -> ( ( y e. x /\ x e. z ) -> y e. z ) )
8	7	expd	|- ( Lim z -> ( y e. x -> ( x e. z -> y e. z ) ) )
9	8	com12	|- ( y e. x -> ( Lim z -> ( x e. z -> y e. z ) ) )
10	9	a2d	|- ( y e. x -> ( ( Lim z -> x e. z ) -> ( Lim z -> y e. z ) ) )
11	10	alimdv	|- ( y e. x -> ( A. z ( Lim z -> x e. z ) -> A. z ( Lim z -> y e. z ) ) )
12	3 11	anim12d	|- ( y e. x -> ( ( x e. On /\ A. z ( Lim z -> x e. z ) ) -> ( y e. On /\ A. z ( Lim z -> y e. z ) ) ) )
13		elom	|- ( x e. _om <-> ( x e. On /\ A. z ( Lim z -> x e. z ) ) )
14		elom	|- ( y e. _om <-> ( y e. On /\ A. z ( Lim z -> y e. z ) ) )
15	12 13 14	3imtr4g	|- ( y e. x -> ( x e. _om -> y e. _om ) )
16	15	imp	|- ( ( y e. x /\ x e. _om ) -> y e. _om )
17	16	ax-gen	|- A. x ( ( y e. x /\ x e. _om ) -> y e. _om )
18	1 17	mpgbir	|- Tr _om
19		omsson	|- _om C_ On
20		ordon	|- Ord On
21		trssord	|- ( ( Tr _om /\ _om C_ On /\ Ord On ) -> Ord _om )
22	18 19 20 21	mp3an	|- Ord _om