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 ) |
| 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 ) |