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)

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

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex1i 
 |-  ( _om ~<_ A -> _om e. _V )
3 nnsdomg 
 |-  ( ( _om e. _V /\ B e. _om ) -> B ~< _om )
4 2 3 sylan 
 |-  ( ( _om ~<_ A /\ B e. _om ) -> B ~< _om )
5 simpl 
 |-  ( ( _om ~<_ A /\ B e. _om ) -> _om ~<_ A )
6 sdomdomtr 
 |-  ( ( B ~< _om /\ _om ~<_ A ) -> B ~< A )
7 4 5 6 syl2anc 
 |-  ( ( _om ~<_ A /\ B e. _om ) -> B ~< A )