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 part of the antecedent. See nnsdom for the version without this sethood requirement. (Contributed by NM, 15-Jun-1998) Avoid ax-pow . (Revised by BTernaryTau, 7-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ordom	|- Ord _om
2		ordelss	|- ( ( Ord _om /\ A e. _om ) -> A C_ _om )
3	1 2	mpan	|- ( A e. _om -> A C_ _om )
4	3	adantr	|- ( ( A e. _om /\ _om e. _V ) -> A C_ _om )
5		nnfi	|- ( A e. _om -> A e. Fin )
6		ssdomfi2	|- ( ( A e. Fin /\ _om e. _V /\ A C_ _om ) -> A ~<_ _om )
7	5 6	syl3an1	|- ( ( A e. _om /\ _om e. _V /\ A C_ _om ) -> A ~<_ _om )
8	4 7	mpd3an3	|- ( ( A e. _om /\ _om e. _V ) -> A ~<_ _om )
9	8	ancoms	|- ( ( _om e. _V /\ A e. _om ) -> A ~<_ _om )
10		ominf	|- -. _om e. Fin
11		ensymfib	|- ( A e. Fin -> ( A ~~ _om <-> _om ~~ A ) )
12	5 11	syl	|- ( A e. _om -> ( A ~~ _om <-> _om ~~ A ) )
13		breq2	|- ( x = A -> ( _om ~~ x <-> _om ~~ A ) )
14	13	rspcev	|- ( ( A e. _om /\ _om ~~ A ) -> E. x e. _om _om ~~ x )
15		isfi	|- ( _om e. Fin <-> E. x e. _om _om ~~ x )
16	14 15	sylibr	|- ( ( A e. _om /\ _om ~~ A ) -> _om e. Fin )
17	16	ex	|- ( A e. _om -> ( _om ~~ A -> _om e. Fin ) )
18	12 17	sylbid	|- ( A e. _om -> ( A ~~ _om -> _om e. Fin ) )
19	10 18	mtoi	|- ( A e. _om -> -. A ~~ _om )
20	19	adantl	|- ( ( _om e. _V /\ A e. _om ) -> -. A ~~ _om )
21		brsdom	|- ( A ~< _om <-> ( A ~<_ _om /\ -. A ~~ _om ) )
22	9 20 21	sylanbrc	|- ( ( _om e. _V /\ A e. _om ) -> A ~< _om )