Metamath Proof Explorer


Theorem trclfvcotr

Description: The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020)

Ref Expression
Assertion trclfvcotr R V t+ R t+ R t+ R

Proof

Step Hyp Ref Expression
1 cotr r r r a b c a r b b r c a r c
2 sp a b c a r b b r c a r c b c a r b b r c a r c
3 2 19.21bbi a b c a r b b r c a r c a r b b r c a r c
4 1 3 sylbi r r r a r b b r c a r c
5 4 adantl R r r r r a r b b r c a r c
6 5 a2i R r r r r a r b b r c R r r r r a r c
7 6 alimi r R r r r r a r b b r c r R r r r r a r c
8 7 ax-gen c r R r r r r a r b b r c r R r r r r a r c
9 8 ax-gen b c r R r r r r a r b b r c r R r r r r a r c
10 9 ax-gen a b c r R r r r r a r b b r c r R r r r r a r c
11 brtrclfv R V a t+ R b r R r r r r a r b
12 brtrclfv R V b t+ R c r R r r r r b r c
13 11 12 anbi12d R V a t+ R b b t+ R c r R r r r r a r b r R r r r r b r c
14 jcab R r r r r a r b b r c R r r r r a r b R r r r r b r c
15 14 albii r R r r r r a r b b r c r R r r r r a r b R r r r r b r c
16 19.26 r R r r r r a r b R r r r r b r c r R r r r r a r b r R r r r r b r c
17 15 16 bitri r R r r r r a r b b r c r R r r r r a r b r R r r r r b r c
18 13 17 bitr4di R V a t+ R b b t+ R c r R r r r r a r b b r c
19 brtrclfv R V a t+ R c r R r r r r a r c
20 18 19 imbi12d R V a t+ R b b t+ R c a t+ R c r R r r r r a r b b r c r R r r r r a r c
21 20 albidv R V c a t+ R b b t+ R c a t+ R c c r R r r r r a r b b r c r R r r r r a r c
22 21 2albidv R V a b c a t+ R b b t+ R c a t+ R c a b c r R r r r r a r b b r c r R r r r r a r c
23 10 22 mpbiri R V a b c a t+ R b b t+ R c a t+ R c
24 cotr t+ R t+ R t+ R a b c a t+ R b b t+ R c a t+ R c
25 23 24 sylibr R V t+ R t+ R t+ R