# 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 ${⊢}\left({A}\preccurlyeq {B}\wedge {B}\preccurlyeq {C}\right)\to {A}\preccurlyeq {C}$

### Proof

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