Theorem dfttrcl2

Description: When R is a set and a relation, then its transitive closure can be defined by an intersection. (Contributed by Scott Fenton, 26-Oct-2024)

	Ref	Expression
Assertion	dfttrcl2	|- ( ( R e. V /\ Rel R ) -> t++ R = |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } )

Proof

Step	Hyp	Ref	Expression
1		ssintab	|- ( t++ R C_ |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } <-> A. z ( ( R C_ z /\ ( z o. z ) C_ z ) -> t++ R C_ z ) )
2		ttrclss	|- ( ( R C_ z /\ ( z o. z ) C_ z ) -> t++ R C_ z )
3	1 2	mpgbir	|- t++ R C_ |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) }
4	3	a1i	|- ( ( R e. V /\ Rel R ) -> t++ R C_ |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } )
5		rabab	|- { z e. _V | ( R C_ z /\ ( z o. z ) C_ z ) } = { z | ( R C_ z /\ ( z o. z ) C_ z ) }
6	5	inteqi	|- |^| { z e. _V | ( R C_ z /\ ( z o. z ) C_ z ) } = |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) }
7		ttrclexg	|- ( R e. V -> t++ R e. _V )
8		ssttrcl	|- ( Rel R -> R C_ t++ R )
9		ttrcltr	|- ( t++ R o. t++ R ) C_ t++ R
10	8 9	jctir	|- ( Rel R -> ( R C_ t++ R /\ ( t++ R o. t++ R ) C_ t++ R ) )
11		sseq2	|- ( z = t++ R -> ( R C_ z <-> R C_ t++ R ) )
12		coeq1	|- ( z = t++ R -> ( z o. z ) = ( t++ R o. z ) )
13		coeq2	|- ( z = t++ R -> ( t++ R o. z ) = ( t++ R o. t++ R ) )
14	12 13	eqtrd	|- ( z = t++ R -> ( z o. z ) = ( t++ R o. t++ R ) )
15		id	|- ( z = t++ R -> z = t++ R )
16	14 15	sseq12d	|- ( z = t++ R -> ( ( z o. z ) C_ z <-> ( t++ R o. t++ R ) C_ t++ R ) )
17	11 16	anbi12d	|- ( z = t++ R -> ( ( R C_ z /\ ( z o. z ) C_ z ) <-> ( R C_ t++ R /\ ( t++ R o. t++ R ) C_ t++ R ) ) )
18	17	intminss	|- ( ( t++ R e. _V /\ ( R C_ t++ R /\ ( t++ R o. t++ R ) C_ t++ R ) ) -> |^| { z e. _V | ( R C_ z /\ ( z o. z ) C_ z ) } C_ t++ R )
19	7 10 18	syl2an	|- ( ( R e. V /\ Rel R ) -> |^| { z e. _V | ( R C_ z /\ ( z o. z ) C_ z ) } C_ t++ R )
20	6 19	eqsstrrid	|- ( ( R e. V /\ Rel R ) -> |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } C_ t++ R )
21	4 20	eqssd	|- ( ( R e. V /\ Rel R ) -> t++ R = |^| { z | ( R C_ z /\ ( z o. z ) C_ z ) } )