Metamath Proof Explorer

Theorem vtoclr

Description: Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses vtoclr.1 
|- Rel R
vtoclr.2 
|- ( ( x R y /\ y R z ) -> x R z )
Assertion vtoclr 
|- ( ( A R B /\ B R C ) -> A R C )

Proof

Step Hyp Ref Expression
1 vtoclr.1 
 |-  Rel R
2 vtoclr.2 
 |-  ( ( x R y /\ y R z ) -> x R z )
3 1 brrelex12i 
 |-  ( A R B -> ( A e. _V /\ B e. _V ) )
4 1 brrelex2i 
 |-  ( B R C -> C e. _V )
5 breq1 
 |-  ( x = A -> ( x R y <-> A R y ) )
6 5 anbi1d 
 |-  ( x = A -> ( ( x R y /\ y R C ) <-> ( A R y /\ y R C ) ) )
7 breq1 
 |-  ( x = A -> ( x R C <-> A R C ) )
8 6 7 imbi12d 
 |-  ( x = A -> ( ( ( x R y /\ y R C ) -> x R C ) <-> ( ( A R y /\ y R C ) -> A R C ) ) )
9 8 imbi2d 
 |-  ( x = A -> ( ( C e. _V -> ( ( x R y /\ y R C ) -> x R C ) ) <-> ( C e. _V -> ( ( A R y /\ y R C ) -> A R C ) ) ) )
10 breq2 
 |-  ( y = B -> ( A R y <-> A R B ) )
11 breq1 
 |-  ( y = B -> ( y R C <-> B R C ) )
12 10 11 anbi12d 
 |-  ( y = B -> ( ( A R y /\ y R C ) <-> ( A R B /\ B R C ) ) )
13 12 imbi1d 
 |-  ( y = B -> ( ( ( A R y /\ y R C ) -> A R C ) <-> ( ( A R B /\ B R C ) -> A R C ) ) )
14 13 imbi2d 
 |-  ( y = B -> ( ( C e. _V -> ( ( A R y /\ y R C ) -> A R C ) ) <-> ( C e. _V -> ( ( A R B /\ B R C ) -> A R C ) ) ) )
15 breq2 
 |-  ( z = C -> ( y R z <-> y R C ) )
16 15 anbi2d 
 |-  ( z = C -> ( ( x R y /\ y R z ) <-> ( x R y /\ y R C ) ) )
17 breq2 
 |-  ( z = C -> ( x R z <-> x R C ) )
18 16 17 imbi12d 
 |-  ( z = C -> ( ( ( x R y /\ y R z ) -> x R z ) <-> ( ( x R y /\ y R C ) -> x R C ) ) )
19 18 2 vtoclg 
 |-  ( C e. _V -> ( ( x R y /\ y R C ) -> x R C ) )
20 9 14 19 vtocl2g 
 |-  ( ( A e. _V /\ B e. _V ) -> ( C e. _V -> ( ( A R B /\ B R C ) -> A R C ) ) )
21 3 4 20 syl2im 
 |-  ( A R B -> ( B R C -> ( ( A R B /\ B R C ) -> A R C ) ) )
22 21 imp 
 |-  ( ( A R B /\ B R C ) -> ( ( A R B /\ B R C ) -> A R C ) )
23 22 pm2.43i 
 |-  ( ( A R B /\ B R C ) -> A R C )