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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnfi | ||
2 | 1 | adantl | |
3 | reldom | ||
4 | 3 | brrelex1i | |
5 | nnsdomg | ||
6 | 4 5 | sylan | |
7 | simpl | ||
8 | sdomdomtrfi | ||
9 | 2 6 7 8 | syl3anc |