This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ω \to (A ≺ B \leftrightarrow suc A ≼ B)$

Proof

Step	Hyp	Ref	Expression
1		sucdom2	$⊢ A ≺ B \to suc A ≼ B$
2		nnfi	$⊢ A \in ω \to A \in Fin$
3		php4	$⊢ A \in ω \to A ≺ suc A$
4		sdomdomtrfi	$⊢ (A \in Fin \land A ≺ suc A \land suc A ≼ B) \to A ≺ B$
5	4	3expia	$⊢ (A \in Fin \land A ≺ suc A) \to (suc A ≼ B \to A ≺ B)$
6	2 3 5	syl2anc	$⊢ A \in ω \to (suc A ≼ B \to A ≺ B)$
7	1 6	impbid2	$⊢ A \in ω \to (A ≺ B \leftrightarrow suc A ≼ B)$