Theorem brcnvtrclfv

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

	Ref	Expression
Assertion	brcnvtrclfv	|- ( ( 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 ) ) )

Proof

Step	Hyp	Ref	Expression
1		brcnvg	|- ( ( A e. V /\ B e. W ) -> ( A `' ( t+ ` R ) B <-> B ( t+ ` R ) A ) )
2	1	3adant1	|- ( ( R e. U /\ A e. V /\ B e. W ) -> ( A `' ( t+ ` R ) B <-> B ( t+ ` R ) A ) )
3		brtrclfv	|- ( R e. U -> ( B ( t+ ` R ) A <-> A. r ( ( R C_ r /\ ( r o. r ) C_ r ) -> B r A ) ) )
4	3	3ad2ant1	|- ( ( R e. U /\ A e. V /\ B e. W ) -> ( B ( t+ ` R ) A <-> A. r ( ( R C_ r /\ ( r o. r ) C_ r ) -> B r A ) ) )
5	2 4	bitrd	|- ( ( 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 ) ) )