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 )