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 e. _V
3	2	brdom	|- ( x ~<_ y <-> E. g g : x -1-1-> y )
4		vex	|- z e. _V
5	4	brdom	|- ( y ~<_ z <-> E. f f : y -1-1-> z )
6		exdistrv	|- ( E. g E. 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	|- ( ( f : y -1-1-> z /\ g : x -1-1-> y ) -> ( f o. g ) : x -1-1-> z )
8	7	ancoms	|- ( ( g : x -1-1-> y /\ f : y -1-1-> z ) -> ( f o. g ) : x -1-1-> z )
9		vex	|- f e. _V
10		vex	|- g e. _V
11	9 10	coex	|- ( f o. g ) e. _V
12		f1eq1	|- ( h = ( f o. g ) -> ( h : x -1-1-> z <-> ( f o. g ) : x -1-1-> z ) )
13	11 12	spcev	|- ( ( f o. g ) : x -1-1-> z -> E. h h : x -1-1-> z )
14	8 13	syl	|- ( ( g : x -1-1-> y /\ f : y -1-1-> z ) -> E. h h : x -1-1-> z )
15	4	brdom	|- ( x ~<_ z <-> E. 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	|- ( E. g E. f ( g : x -1-1-> y /\ f : y -1-1-> z ) -> x ~<_ z )
18	6 17	sylbir	|- ( ( E. g g : x -1-1-> y /\ E. 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 )