Metamath Proof Explorer


Theorem infsdomnn

Description: An infinite set strictly dominates a natural number. (Contributed by NM, 22-Nov-2004) (Revised by Mario Carneiro, 27-Apr-2015) Avoid ax-pow . (Revised by BTernaryTau, 7-Jan-2025)

Ref Expression
Assertion infsdomnn
|- ( ( _om ~<_ A /\ B e. _om ) -> B ~< A )

Proof

Step Hyp Ref Expression
1 nnfi
 |-  ( B e. _om -> B e. Fin )
2 1 adantl
 |-  ( ( _om ~<_ A /\ B e. _om ) -> B e. Fin )
3 reldom
 |-  Rel ~<_
4 3 brrelex1i
 |-  ( _om ~<_ A -> _om e. _V )
5 nnsdomg
 |-  ( ( _om e. _V /\ B e. _om ) -> B ~< _om )
6 4 5 sylan
 |-  ( ( _om ~<_ A /\ B e. _om ) -> B ~< _om )
7 simpl
 |-  ( ( _om ~<_ A /\ B e. _om ) -> _om ~<_ A )
8 sdomdomtrfi
 |-  ( ( B e. Fin /\ B ~< _om /\ _om ~<_ A ) -> B ~< A )
9 2 6 7 8 syl3anc
 |-  ( ( _om ~<_ A /\ B e. _om ) -> B ~< A )