domtrfi

Description: Transitivity of dominance relation for finite sets, proved without using the Axiom of Power Sets (unlike domtr ). (Contributed by BTernaryTau, 17-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		domfi	$⊢ (C \in Fin \land B ≼ C) \to B \in Fin$
2		brdomg	$⊢ B \in Fin \to (A ≼ B \leftrightarrow \exists g g : A \underset{1-1}{⟶} B)$
3	2	biimpa	$⊢ (B \in Fin \land A ≼ B) \to \exists g g : A \underset{1-1}{⟶} B$
4	1 3	stoic3	$⊢ (C \in Fin \land B ≼ C \land A ≼ B) \to \exists g g : A \underset{1-1}{⟶} B$
5	4	3com23	$⊢ (C \in Fin \land A ≼ B \land B ≼ C) \to \exists g g : A \underset{1-1}{⟶} B$
6		brdomg	$⊢ C \in Fin \to (B ≼ C \leftrightarrow \exists f f : B \underset{1-1}{⟶} C)$
7	6	biimpa	$⊢ (C \in Fin \land B ≼ C) \to \exists f f : B \underset{1-1}{⟶} C$
8	7	3adant2	$⊢ (C \in Fin \land \exists g g : A \underset{1-1}{⟶} B \land B ≼ C) \to \exists f f : B \underset{1-1}{⟶} C$
9		exdistrv	$⊢ \exists g \exists f (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C) \leftrightarrow (\exists g g : A \underset{1-1}{⟶} B \land \exists f f : B \underset{1-1}{⟶} C)$
10		19.42vv	$⊢ \exists g \exists f (C \in Fin \land (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C)) \leftrightarrow (C \in Fin \land \exists g \exists f (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C))$
11		f1co	$⊢ (f : B \underset{1-1}{⟶} C \land g : A \underset{1-1}{⟶} B) \to (f \circ g) : A \underset{1-1}{⟶} C$
12	11	ancoms	$⊢ (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C) \to (f \circ g) : A \underset{1-1}{⟶} C$
13		f1domfi	$⊢ (C \in Fin \land (f \circ g) : A \underset{1-1}{⟶} C) \to A ≼ C$
14	12 13	sylan2	$⊢ (C \in Fin \land (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C)) \to A ≼ C$
15	14	exlimivv	$⊢ \exists g \exists f (C \in Fin \land (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C)) \to A ≼ C$
16	10 15	sylbir	$⊢ (C \in Fin \land \exists g \exists f (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C)) \to A ≼ C$
17	9 16	sylan2br	$⊢ (C \in Fin \land (\exists g g : A \underset{1-1}{⟶} B \land \exists f f : B \underset{1-1}{⟶} C)) \to A ≼ C$
18	17	3impb	$⊢ (C \in Fin \land \exists g g : A \underset{1-1}{⟶} B \land \exists f f : B \underset{1-1}{⟶} C) \to A ≼ C$
19	8 18	syld3an3	$⊢ (C \in Fin \land \exists g g : A \underset{1-1}{⟶} B \land B ≼ C) \to A ≼ C$
20	5 19	syld3an2	$⊢ (C \in Fin \land A ≼ B \land B ≼ C) \to A ≼ C$

Metamath Proof Explorer

Theorem domtrfi

Proof