Description: Strict dominance of a set over a natural number is the same as dominance over its successor. (Contributed by Mario Carneiro, 12-Jan-2013) Avoid ax-pow . (Revised by BTernaryTau, 4-Dec-2024) (Proof shortened by BJ, 11-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sucdom | |- ( A e. _om -> ( A ~< B <-> suc A ~<_ B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sucdom2 | |- ( A ~< B -> suc A ~<_ B ) |
|
| 2 | nnfi | |- ( A e. _om -> A e. Fin ) |
|
| 3 | php4 | |- ( A e. _om -> A ~< suc A ) |
|
| 4 | sdomdomtrfi | |- ( ( A e. Fin /\ A ~< suc A /\ suc A ~<_ B ) -> A ~< B ) |
|
| 5 | 4 | 3expia | |- ( ( A e. Fin /\ A ~< suc A ) -> ( suc A ~<_ B -> A ~< B ) ) |
| 6 | 2 3 5 | syl2anc | |- ( A e. _om -> ( suc A ~<_ B -> A ~< B ) ) |
| 7 | 1 6 | impbid2 | |- ( A e. _om -> ( A ~< B <-> suc A ~<_ B ) ) |