This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )

Proof

Step Hyp Ref Expression
1 reldom ⊢ Rel ≼
2 vex ⊢ 𝑦 ∈ V
3 2 brdom ⊢ ( 𝑥 ≼ 𝑦 ↔ ∃ 𝑔 𝑔 : 𝑥 –1-1→ 𝑦 )
4 vex ⊢ 𝑧 ∈ V
5 4 brdom ⊢ ( 𝑦 ≼ 𝑧 ↔ ∃ 𝑓 𝑓 : 𝑦 –1-1→ 𝑧 )
6 exdistrv ⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) ↔ ( ∃ 𝑔 𝑔 : 𝑥 –1-1→ 𝑦 ∧ ∃ 𝑓 𝑓 : 𝑦 –1-1→ 𝑧 ) )
7 f1co ⊢ ( ( 𝑓 : 𝑦 –1-1→ 𝑧 ∧ 𝑔 : 𝑥 –1-1→ 𝑦 ) → ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1→ 𝑧 )
8 7 ancoms ⊢ ( ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) → ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1→ 𝑧 )
9 vex ⊢ 𝑓 ∈ V
10 vex ⊢ 𝑔 ∈ V
11 9 10 coex ⊢ ( 𝑓 ∘ 𝑔 ) ∈ V
12 f1eq1 ⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( ℎ : 𝑥 –1-1→ 𝑧 ↔ ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1→ 𝑧 ) )
13 11 12 spcev ⊢ ( ( 𝑓 ∘ 𝑔 ) : 𝑥 –1-1→ 𝑧 → ∃ ℎ ℎ : 𝑥 –1-1→ 𝑧 )
14 8 13 syl ⊢ ( ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) → ∃ ℎ ℎ : 𝑥 –1-1→ 𝑧 )
15 4 brdom ⊢ ( 𝑥 ≼ 𝑧 ↔ ∃ ℎ ℎ : 𝑥 –1-1→ 𝑧 )
16 14 15 sylibr ⊢ ( ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) → 𝑥 ≼ 𝑧 )
17 16 exlimivv ⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑔 : 𝑥 –1-1→ 𝑦 ∧ 𝑓 : 𝑦 –1-1→ 𝑧 ) → 𝑥 ≼ 𝑧 )
18 6 17 sylbir ⊢ ( ( ∃ 𝑔 𝑔 : 𝑥 –1-1→ 𝑦 ∧ ∃ 𝑓 𝑓 : 𝑦 –1-1→ 𝑧 ) → 𝑥 ≼ 𝑧 )
19 3 5 18 syl2anb ⊢ ( ( 𝑥 ≼ 𝑦 ∧ 𝑦 ≼ 𝑧 ) → 𝑥 ≼ 𝑧 )
20 1 19 vtoclr ⊢ ( ( 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐶 ) → 𝐴 ≼ 𝐶 )