Metamath Proof Explorer

Theorem 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 ∧ B ≼ C → A ≼ C

Proof

Step Hyp Ref Expression
1 reldom ⊢ Rel ⁡ ≼
2 vex ⊢ y ∈ V
3 2 brdom ⊢ x ≼ y ↔ ∃ g g : x ⟶ 1-1 y
4 vex ⊢ z ∈ V
5 4 brdom ⊢ y ≼ z ↔ ∃ f f : y ⟶ 1-1 z
6 exdistrv ⊢ ∃ g ∃ f g : x ⟶ 1-1 y ∧ f : y ⟶ 1-1 z ↔ ∃ g g : x ⟶ 1-1 y ∧ ∃ f f : y ⟶ 1-1 z
7 f1co ⊢ f : y ⟶ 1-1 z ∧ g : x ⟶ 1-1 y → f ∘ g : x ⟶ 1-1 z
8 7 ancoms ⊢ g : x ⟶ 1-1 y ∧ f : y ⟶ 1-1 z → f ∘ g : x ⟶ 1-1 z
9 vex ⊢ f ∈ V
10 vex ⊢ g ∈ V
11 9 10 coex ⊢ f ∘ g ∈ V
12 f1eq1 ⊢ h = f ∘ g → h : x ⟶ 1-1 z ↔ f ∘ g : x ⟶ 1-1 z
13 11 12 spcev ⊢ f ∘ g : x ⟶ 1-1 z → ∃ h h : x ⟶ 1-1 z
14 8 13 syl ⊢ g : x ⟶ 1-1 y ∧ f : y ⟶ 1-1 z → ∃ h h : x ⟶ 1-1 z
15 4 brdom ⊢ x ≼ z ↔ ∃ h h : x ⟶ 1-1 z
16 14 15 sylibr ⊢ g : x ⟶ 1-1 y ∧ f : y ⟶ 1-1 z → x ≼ z
17 16 exlimivv ⊢ ∃ g ∃ f g : x ⟶ 1-1 y ∧ f : y ⟶ 1-1 z → x ≼ z
18 6 17 sylbir ⊢ ∃ g g : x ⟶ 1-1 y ∧ ∃ f f : y ⟶ 1-1 z → x ≼ z
19 3 5 18 syl2anb ⊢ x ≼ y ∧ y ≼ z → x ≼ z
20 1 19 vtoclr ⊢ A ≼ B ∧ B ≼ C → A ≼ C