Metamath Proof Explorer


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 )