Theorem ssnlim

Description: An ordinal subclass of non-limit ordinals is a class of natural numbers. Exercise 7 of TakeutiZaring p. 42. (Contributed by NM, 2-Nov-2004)

	Ref	Expression
Assertion	ssnlim	|- ( ( Ord A /\ A C_ { x e. On | -. Lim x } ) -> A C_ _om )

Proof

Step	Hyp	Ref	Expression
1		limom	|- Lim _om
2		ssel	|- ( A C_ { x e. On | -. Lim x } -> ( _om e. A -> _om e. { x e. On | -. Lim x } ) )
3		limeq	|- ( x = _om -> ( Lim x <-> Lim _om ) )
4	3	notbid	|- ( x = _om -> ( -. Lim x <-> -. Lim _om ) )
5	4	elrab	|- ( _om e. { x e. On | -. Lim x } <-> ( _om e. On /\ -. Lim _om ) )
6	5	simprbi	|- ( _om e. { x e. On | -. Lim x } -> -. Lim _om )
7	2 6	syl6	|- ( A C_ { x e. On | -. Lim x } -> ( _om e. A -> -. Lim _om ) )
8	1 7	mt2i	|- ( A C_ { x e. On | -. Lim x } -> -. _om e. A )
9	8	adantl	|- ( ( Ord A /\ A C_ { x e. On | -. Lim x } ) -> -. _om e. A )
10		ordom	|- Ord _om
11		ordtri1	|- ( ( Ord A /\ Ord _om ) -> ( A C_ _om <-> -. _om e. A ) )
12	10 11	mpan2	|- ( Ord A -> ( A C_ _om <-> -. _om e. A ) )
13	12	adantr	|- ( ( Ord A /\ A C_ { x e. On | -. Lim x } ) -> ( A C_ _om <-> -. _om e. A ) )
14	9 13	mpbird	|- ( ( Ord A /\ A C_ { x e. On | -. Lim x } ) -> A C_ _om )