Theorem reftr

Description: Refinement is transitive. (Contributed by Jeff Hankins, 18-Jan-2010) (Revised by Thierry Arnoux, 3-Feb-2020)

	Ref	Expression
Assertion	reftr	|- ( ( A Ref B /\ B Ref C ) -> A Ref C )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- U. B = U. B
2		eqid	|- U. C = U. C
3	1 2	refbas	|- ( B Ref C -> U. C = U. B )
4		eqid	|- U. A = U. A
5	4 1	refbas	|- ( A Ref B -> U. B = U. A )
6	3 5	sylan9eqr	|- ( ( A Ref B /\ B Ref C ) -> U. C = U. A )
7		refssex	|- ( ( A Ref B /\ x e. A ) -> E. y e. B x C_ y )
8	7	ex	|- ( A Ref B -> ( x e. A -> E. y e. B x C_ y ) )
9	8	adantr	|- ( ( A Ref B /\ B Ref C ) -> ( x e. A -> E. y e. B x C_ y ) )
10		refssex	|- ( ( B Ref C /\ y e. B ) -> E. z e. C y C_ z )
11	10	ad2ant2lr	|- ( ( ( A Ref B /\ B Ref C ) /\ ( y e. B /\ x C_ y ) ) -> E. z e. C y C_ z )
12		sstr2	|- ( x C_ y -> ( y C_ z -> x C_ z ) )
13	12	reximdv	|- ( x C_ y -> ( E. z e. C y C_ z -> E. z e. C x C_ z ) )
14	13	ad2antll	|- ( ( ( A Ref B /\ B Ref C ) /\ ( y e. B /\ x C_ y ) ) -> ( E. z e. C y C_ z -> E. z e. C x C_ z ) )
15	11 14	mpd	|- ( ( ( A Ref B /\ B Ref C ) /\ ( y e. B /\ x C_ y ) ) -> E. z e. C x C_ z )
16	15	rexlimdvaa	|- ( ( A Ref B /\ B Ref C ) -> ( E. y e. B x C_ y -> E. z e. C x C_ z ) )
17	9 16	syld	|- ( ( A Ref B /\ B Ref C ) -> ( x e. A -> E. z e. C x C_ z ) )
18	17	ralrimiv	|- ( ( A Ref B /\ B Ref C ) -> A. x e. A E. z e. C x C_ z )
19		refrel	|- Rel Ref
20	19	brrelex1i	|- ( A Ref B -> A e. _V )
21	20	adantr	|- ( ( A Ref B /\ B Ref C ) -> A e. _V )
22	4 2	isref	|- ( A e. _V -> ( A Ref C <-> ( U. C = U. A /\ A. x e. A E. z e. C x C_ z ) ) )
23	21 22	syl	|- ( ( A Ref B /\ B Ref C ) -> ( A Ref C <-> ( U. C = U. A /\ A. x e. A E. z e. C x C_ z ) ) )
24	6 18 23	mpbir2and	|- ( ( A Ref B /\ B Ref C ) -> A Ref C )