Theorem domtr 6201

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

Assertion

Ref	Expression
domtr	|- ((A ~<_ B /\ B ~<_ C) -> A ~<_ C)

Proof of Theorem domtr

Dummy variables x y z f g h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reldom 6162	. 2 |- Rel ~<_
2		vex 2554	. . . 4 |- y e. _V
3	2	brdom 6167	. . 3 |- (x ~<_ y <-> E.g g :x -1-1->y)
4		vex 2554	. . . 4 |- z e. _V
5	4	brdom 6167	. . 3 |- (y ~<_ z <-> E.f f :y -1-1->z)
6		eeanv 1804	. . . 4 |- (E.gE.f(g :x -1-1->y /\ f :y -1-1->z) <-> (E.g g :x -1-1->y /\ E.f f :y -1-1->z))
7		f1co 5044	. . . . . . . 8 |- ((f :y -1-1->z /\ g :x -1-1->y) -> (f o. g) :x -1-1->z)
8	7	ancoms 255	. . . . . . 7 |- ((g :x -1-1->y /\ f :y -1-1->z) -> (f o. g) :x -1-1->z)
9		vex 2554	. . . . . . . . 9 |- f e. _V
10		vex 2554	. . . . . . . . 9 |- g e. _V
11	9, 10	coex 4806	. . . . . . . 8 |- (f o. g) e. _V
12		f1eq1 5030	. . . . . . . 8 |- ( h = (f o. g) -> ( h :x -1-1->z <-> (f o. g) :x -1-1->z))
13	11, 12	spcev 2641	. . . . . . 7 |- ((f o. g) :x -1-1->z -> E. h h :x -1-1->z)
14	8, 13	syl 14	. . . . . 6 |- ((g :x -1-1->y /\ f :y -1-1->z) -> E. h h :x -1-1->z)
15	4	brdom 6167	. . . . . 6 |- (x ~<_ z <-> E. h h :x -1-1->z)
16	14, 15	sylibr 137	. . . . 5 |- ((g :x -1-1->y /\ f :y -1-1->z) -> x ~<_ z)
17	16	exlimivv 1773	. . . 4 |- (E.gE.f(g :x -1-1->y /\ f :y -1-1->z) -> x ~<_ z)
18	6, 17	sylbir 125	. . 3 |- ((E.g g :x -1-1->y /\ E.f f :y -1-1->z) -> x ~<_ z)
19	3, 5, 18	syl2anb 275	. 2 |- ((x ~<_ y /\ y ~<_ z) -> x ~<_ z)
20	1, 19	vtoclr 4331	1 |- ((A ~<_ B /\ B ~<_ C) -> A ~<_ C)

Syntax hints:   -> wi 4   /\ wa 97  E.wex 1378   class class class wbr 3755   o. ccom 4292   -1-1->wf1 4842   ~<_ cdom 6156

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-dom 6159

This theorem is referenced by:  endomtr  6206  domentr  6207