Theorem brtrclfv

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

	Ref	Expression
Assertion	brtrclfv	|- ( 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		trclfv	|- ( R e. V -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
2	1	breqd	|- ( R e. V -> ( A ( t+ ` R ) B <-> A |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } B ) )
3		brintclab	|- ( A |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } B <-> A. r ( ( R C_ r /\ ( r o. r ) C_ r ) -> <. A , B >. e. r ) )
4		df-br	|- ( A r B <-> <. A , B >. e. r )
5	4	imbi2i	|- ( ( ( R C_ r /\ ( r o. r ) C_ r ) -> A r B ) <-> ( ( R C_ r /\ ( r o. r ) C_ r ) -> <. A , B >. e. r ) )
6	5	albii	|- ( A. r ( ( R C_ r /\ ( r o. r ) C_ r ) -> A r B ) <-> A. r ( ( R C_ r /\ ( r o. r ) C_ r ) -> <. A , B >. e. r ) )
7	3 6	bitr4i	|- ( A |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } B <-> A. r ( ( R C_ r /\ ( r o. r ) C_ r ) -> A r B ) )
8	2 7	bitrdi	|- ( R e. V -> ( A ( t+ ` R ) B <-> A. r ( ( R C_ r /\ ( r o. r ) C_ r ) -> A r B ) ) )