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 ) ) )

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 ) ) )

Step

Hyp

Ref

Expression

 |-  ( R e. V -> `' R e. _V )

 |-  ( `' R e. _V -> ( A ( t+ ` `' R ) B <-> A. r ( ( `' R C_ r /\ ( r o. r ) C_ r ) -> A r B ) ) )

1 2

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