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