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 ω V A ω A ω

Proof

Step Hyp Ref Expression
1 ssdomg ω V A ω A ω
2 ordom Ord ω
3 ordelss Ord ω A ω A ω
4 2 3 mpan A ω A ω
5 1 4 impel ω V A ω A ω
6 ominf ¬ ω Fin
7 ensym A ω ω A
8 breq2 x = A ω x ω A
9 8 rspcev A ω ω A x ω ω x
10 isfi ω Fin x ω ω x
11 9 10 sylibr A ω ω A ω Fin
12 11 ex A ω ω A ω Fin
13 7 12 syl5 A ω A ω ω Fin
14 6 13 mtoi A ω ¬ A ω
15 14 adantl ω V A ω ¬ A ω
16 brsdom A ω A ω ¬ A ω
17 5 15 16 sylanbrc ω V A ω A ω