domtr

Description: Transitivity of dominance relation. Theorem 17 of Suppes p. 94. (Contributed by NM, 4-Jun-1998) (Revised by Mario Carneiro, 15-Nov-2014)

		Ref	Expression
	Assertion	domtr	$⊢ (A ≼ B \land B ≼ C) \to A ≼ C$

Proof

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2		vex	$⊢ y \in V$
3	2	brdom	$⊢ x ≼ y \leftrightarrow \exists g g : x \underset{1-1}{⟶} y$
4		vex	$⊢ z \in V$
5	4	brdom	$⊢ y ≼ z \leftrightarrow \exists f f : y \underset{1-1}{⟶} z$
6		exdistrv	$⊢ \exists g \exists f (g : x \underset{1-1}{⟶} y \land f : y \underset{1-1}{⟶} z) \leftrightarrow (\exists g g : x \underset{1-1}{⟶} y \land \exists f f : y \underset{1-1}{⟶} z)$
7		f1co	$⊢ (f : y \underset{1-1}{⟶} z \land g : x \underset{1-1}{⟶} y) \to (f \circ g) : x \underset{1-1}{⟶} z$
8	7	ancoms	$⊢ (g : x \underset{1-1}{⟶} y \land f : y \underset{1-1}{⟶} z) \to (f \circ g) : x \underset{1-1}{⟶} z$
9		vex	$⊢ f \in V$
10		vex	$⊢ g \in V$
11	9 10	coex	$⊢ f \circ g \in V$
12		f1eq1	$⊢ h = f \circ g \to (h : x \underset{1-1}{⟶} z \leftrightarrow (f \circ g) : x \underset{1-1}{⟶} z)$
13	11 12	spcev	$⊢ (f \circ g) : x \underset{1-1}{⟶} z \to \exists h h : x \underset{1-1}{⟶} z$
14	8 13	syl	$⊢ (g : x \underset{1-1}{⟶} y \land f : y \underset{1-1}{⟶} z) \to \exists h h : x \underset{1-1}{⟶} z$
15	4	brdom	$⊢ x ≼ z \leftrightarrow \exists h h : x \underset{1-1}{⟶} z$
16	14 15	sylibr	$⊢ (g : x \underset{1-1}{⟶} y \land f : y \underset{1-1}{⟶} z) \to x ≼ z$
17	16	exlimivv	$⊢ \exists g \exists f (g : x \underset{1-1}{⟶} y \land f : y \underset{1-1}{⟶} z) \to x ≼ z$
18	6 17	sylbir	$⊢ (\exists g g : x \underset{1-1}{⟶} y \land \exists f f : y \underset{1-1}{⟶} z) \to x ≼ z$
19	3 5 18	syl2anb	$⊢ (x ≼ y \land y ≼ z) \to x ≼ z$
20	1 19	vtoclr	$⊢ (A ≼ B \land B ≼ C) \to A ≼ C$

Metamath Proof Explorer

Theorem domtr

Proof