domtrfil

Description: Transitivity of dominance relation when A is finite, proved without using the Axiom of Power Sets (unlike domtr ). (Contributed by BTernaryTau, 24-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2	1	brrelex2i	$⊢ B ≼ C \to C \in V$
3	2	anim2i	$⊢ (A \in Fin \land B ≼ C) \to (A \in Fin \land C \in V)$
4	3	3adant2	$⊢ (A \in Fin \land A ≼ B \land B ≼ C) \to (A \in Fin \land C \in V)$
5		brdomi	$⊢ A ≼ B \to \exists g g : A \underset{1-1}{⟶} B$
6		brdomi	$⊢ B ≼ C \to \exists f f : B \underset{1-1}{⟶} C$
7		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)$
8		19.42vv	$⊢ \exists g \exists f ((A \in Fin \land C \in V) \land (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C)) \leftrightarrow ((A \in Fin \land C \in V) \land \exists g \exists f (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C))$
9		f1co	$⊢ (f : B \underset{1-1}{⟶} C \land g : A \underset{1-1}{⟶} B) \to (f \circ g) : A \underset{1-1}{⟶} C$
10	9	ancoms	$⊢ (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C) \to (f \circ g) : A \underset{1-1}{⟶} C$
11		f1domfi2	$⊢ (A \in Fin \land C \in V \land (f \circ g) : A \underset{1-1}{⟶} C) \to A ≼ C$
12	11	3expa	$⊢ ((A \in Fin \land C \in V) \land (f \circ g) : A \underset{1-1}{⟶} C) \to A ≼ C$
13	10 12	sylan2	$⊢ ((A \in Fin \land C \in V) \land (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C)) \to A ≼ C$
14	13	exlimivv	$⊢ \exists g \exists f ((A \in Fin \land C \in V) \land (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C)) \to A ≼ C$
15	8 14	sylbir	$⊢ ((A \in Fin \land C \in V) \land \exists g \exists f (g : A \underset{1-1}{⟶} B \land f : B \underset{1-1}{⟶} C)) \to A ≼ C$
16	7 15	sylan2br	$⊢ ((A \in Fin \land C \in V) \land (\exists g g : A \underset{1-1}{⟶} B \land \exists f f : B \underset{1-1}{⟶} C)) \to A ≼ C$
17	16	3impb	$⊢ ((A \in Fin \land C \in V) \land \exists g g : A \underset{1-1}{⟶} B \land \exists f f : B \underset{1-1}{⟶} C) \to A ≼ C$
18	6 17	syl3an3	$⊢ ((A \in Fin \land C \in V) \land \exists g g : A \underset{1-1}{⟶} B \land B ≼ C) \to A ≼ C$
19	5 18	syl3an2	$⊢ ((A \in Fin \land C \in V) \land A ≼ B \land B ≼ C) \to A ≼ C$
20	4 19	syld3an1	$⊢ (A \in Fin \land A ≼ B \land B ≼ C) \to A ≼ C$

Metamath Proof Explorer

Theorem domtrfil

Proof