Theorem cotrtrclfv

Description: The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020)

	Ref	Expression
Assertion	cotrtrclfv	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> ( t+ ` R ) = R )

Proof

Step	Hyp	Ref	Expression
1		trclfv	|- ( R e. V -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
2	1	adantr	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> ( t+ ` R ) = |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
3		simpr	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> ( R o. R ) C_ R )
4		ssid	|- R C_ R
5	3 4	jctil	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> ( R C_ R /\ ( R o. R ) C_ R ) )
6		trcleq2lem	|- ( r = R -> ( ( R C_ r /\ ( r o. r ) C_ r ) <-> ( R C_ R /\ ( R o. R ) C_ R ) ) )
7	6	elabg	|- ( R e. V -> ( R e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } <-> ( R C_ R /\ ( R o. R ) C_ R ) ) )
8	7	adantr	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> ( R e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } <-> ( R C_ R /\ ( R o. R ) C_ R ) ) )
9	5 8	mpbird	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> R e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } )
10		intss1	|- ( R e. { r | ( R C_ r /\ ( r o. r ) C_ r ) } -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ R )
11	9 10	syl	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ R )
12	2 11	eqsstrd	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> ( t+ ` R ) C_ R )
13		trclfvlb	|- ( R e. V -> R C_ ( t+ ` R ) )
14	13	adantr	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> R C_ ( t+ ` R ) )
15	12 14	eqssd	|- ( ( R e. V /\ ( R o. R ) C_ R ) -> ( t+ ` R ) = R )