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

Proof

Step Hyp Ref Expression
1 nnfi B ω B Fin
2 1 adantl ω A B ω B Fin
3 reldom Rel
4 3 brrelex1i ω A ω V
5 nnsdomg ω V B ω B ω
6 4 5 sylan ω A B ω B ω
7 simpl ω A B ω ω A
8 sdomdomtrfi B Fin B ω ω A B A
9 2 6 7 8 syl3anc ω A B ω B A