Theorem sucdom

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\in \mathrm{\omega }\to \left(A\prec B\leftrightarrow \mathrm{suc}A\preccurlyeq B\right)$$

Proof

Step	Hyp	Ref	Expression
1		sucdom2	$$⊢A\prec B\to \mathrm{suc}A\preccurlyeq B$$
2		nnfi	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{Fin}$$
3		php4	$$⊢A\in \mathrm{\omega }\to A\prec \mathrm{suc}A$$
4		sdomdomtrfi	$$⊢\left(A\in \mathrm{Fin}\wedge A\prec \mathrm{suc}A\wedge \mathrm{suc}A\preccurlyeq B\right)\to A\prec B$$
5	4	3expia	$$⊢\left(A\in \mathrm{Fin}\wedge A\prec \mathrm{suc}A\right)\to \left(\mathrm{suc}A\preccurlyeq B\to A\prec B\right)$$
6	2 3 5	syl2anc	$$⊢A\in \mathrm{\omega }\to \left(\mathrm{suc}A\preccurlyeq B\to A\prec B\right)$$
7	1 6	impbid2	$$⊢A\in \mathrm{\omega }\to \left(A\prec B\leftrightarrow \mathrm{suc}A\preccurlyeq B\right)$$