Metamath Proof Explorer


Theorem nnsdomg

Description: Omega strictly dominates a natural number. Example 3 of Enderton p. 146. In order to avoid the Axiom of infinity, we include it as a hypothesis. (Contributed by NM, 15-Jun-1998)

Ref Expression
Assertion nnsdomg
|- ( ( _om e. _V /\ A e. _om ) -> A ~< _om )

Proof

Step Hyp Ref Expression
1 ssdomg
 |-  ( _om e. _V -> ( A C_ _om -> A ~<_ _om ) )
2 ordom
 |-  Ord _om
3 ordelss
 |-  ( ( Ord _om /\ A e. _om ) -> A C_ _om )
4 2 3 mpan
 |-  ( A e. _om -> A C_ _om )
5 1 4 impel
 |-  ( ( _om e. _V /\ A e. _om ) -> A ~<_ _om )
6 ominf
 |-  -. _om e. Fin
7 ensym
 |-  ( A ~~ _om -> _om ~~ A )
8 breq2
 |-  ( x = A -> ( _om ~~ x <-> _om ~~ A ) )
9 8 rspcev
 |-  ( ( A e. _om /\ _om ~~ A ) -> E. x e. _om _om ~~ x )
10 isfi
 |-  ( _om e. Fin <-> E. x e. _om _om ~~ x )
11 9 10 sylibr
 |-  ( ( A e. _om /\ _om ~~ A ) -> _om e. Fin )
12 11 ex
 |-  ( A e. _om -> ( _om ~~ A -> _om e. Fin ) )
13 7 12 syl5
 |-  ( A e. _om -> ( A ~~ _om -> _om e. Fin ) )
14 6 13 mtoi
 |-  ( A e. _om -> -. A ~~ _om )
15 14 adantl
 |-  ( ( _om e. _V /\ A e. _om ) -> -. A ~~ _om )
16 brsdom
 |-  ( A ~< _om <-> ( A ~<_ _om /\ -. A ~~ _om ) )
17 5 15 16 sylanbrc
 |-  ( ( _om e. _V /\ A e. _om ) -> A ~< _om )