Metamath Proof Explorer

Theorem brcnvtrclfvcnv

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

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

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

Step

Hyp

Ref

Expression

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

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

1 2

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