Metamath Proof Explorer


Theorem brtrclfvcnv

Description: Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020)

Ref Expression
Assertion brtrclfvcnv
|- ( R e. V -> ( A ( t+ ` `' R ) B <-> A. r ( ( `' R C_ r /\ ( r o. r ) C_ r ) -> A r B ) ) )

Proof

Step Hyp Ref Expression
1 cnvexg
 |-  ( R e. V -> `' R e. _V )
2 brtrclfv
 |-  ( `' R e. _V -> ( A ( t+ ` `' R ) B <-> A. r ( ( `' R C_ r /\ ( r o. r ) C_ r ) -> A r B ) ) )
3 1 2 syl
 |-  ( R e. V -> ( A ( t+ ` `' R ) B <-> A. r ( ( `' R C_ r /\ ( r o. r ) C_ r ) -> A r B ) ) )