This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) } )