sdomdomtrfi

Description: Transitivity of strict dominance and dominance when A is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr ). (Contributed by BTernaryTau, 25-Nov-2024)

		Ref	Expression
	Assertion	sdomdomtrfi	$⊢ (A \in Fin \land A ≺ B \land B ≼ C) \to A ≺ C$

Proof

Step	Hyp	Ref	Expression
1		sdomdom	$⊢ A ≺ B \to A ≼ B$
2		domtrfil	$⊢ (A \in Fin \land A ≼ B \land B ≼ C) \to A ≼ C$
3	1 2	syl3an2	$⊢ (A \in Fin \land A ≺ B \land B ≼ C) \to A ≼ C$
4		simp1	$⊢ (A \in Fin \land B ≼ C \land A \approx C) \to A \in Fin$
5		ensymfib	$⊢ A \in Fin \to (A \approx C \leftrightarrow C \approx A)$
6	5	biimpa	$⊢ (A \in Fin \land A \approx C) \to C \approx A$
7	6	3adant2	$⊢ (A \in Fin \land B ≼ C \land A \approx C) \to C \approx A$
8		endom	$⊢ C \approx A \to C ≼ A$
9		domtrfir	$⊢ (A \in Fin \land B ≼ C \land C ≼ A) \to B ≼ A$
10	8 9	syl3an3	$⊢ (A \in Fin \land B ≼ C \land C \approx A) \to B ≼ A$
11	7 10	syld3an3	$⊢ (A \in Fin \land B ≼ C \land A \approx C) \to B ≼ A$
12		domfi	$⊢ (A \in Fin \land B ≼ A) \to B \in Fin$
13		domnsymfi	$⊢ (B \in Fin \land B ≼ A) \to \neg A ≺ B$
14	12 13	sylancom	$⊢ (A \in Fin \land B ≼ A) \to \neg A ≺ B$
15	4 11 14	syl2anc	$⊢ (A \in Fin \land B ≼ C \land A \approx C) \to \neg A ≺ B$
16	15	3expia	$⊢ (A \in Fin \land B ≼ C) \to (A \approx C \to \neg A ≺ B)$
17	16	con2d	$⊢ (A \in Fin \land B ≼ C) \to (A ≺ B \to \neg A \approx C)$
18	17	3impia	$⊢ (A \in Fin \land B ≼ C \land A ≺ B) \to \neg A \approx C$
19	18	3com23	$⊢ (A \in Fin \land A ≺ B \land B ≼ C) \to \neg A \approx C$
20		brsdom	$⊢ A ≺ C \leftrightarrow (A ≼ C \land \neg A \approx C)$
21	3 19 20	sylanbrc	$⊢ (A \in Fin \land A ≺ B \land B ≼ C) \to A ≺ C$

Metamath Proof Explorer

Theorem sdomdomtrfi

Proof