This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )