Metamath Proof Explorer

Theorem nnsdom

Description: A natural number is strictly dominated by the set of natural numbers. Example 3 of Enderton p. 146. (Contributed by NM, 28-Oct-2003)

Ref Expression
Assertion nnsdom 
|- ( A e. _om -> A ~< _om )

Proof

Step Hyp Ref Expression
1 omex 
 |-  _om e. _V
2 nnsdomg 
 |-  ( ( _om e. _V /\ A e. _om ) -> A ~< _om )
3 1 2 mpan 
 |-  ( A e. _om -> A ~< _om )