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 e. V -> ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R ) )

Proof

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