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

Metamath Proof Explorer

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 )