Metamath Proof Explorer

Theorem dfttc3gw

Description: If the transitive closure of A is a set, then its value is ( TCA ) . If we assume Transitive Containment, then we can weaken the hypothesis to A e. V , see dfttc3g . (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion dfttc3gw 
|- ( TC+ A e. V -> TC+ A = ( TC ` A ) )

Proof

Step Hyp Ref Expression
1 ssmin 
 |-  A C_ |^| { y | ( A C_ y /\ Tr y ) }
2 treq 
 |-  ( x = y -> ( Tr x <-> Tr y ) )
3 2 ralab2 
 |-  ( A. x e. { y | ( A C_ y /\ Tr y ) } Tr x <-> A. y ( ( A C_ y /\ Tr y ) -> Tr y ) )
4 simpr 
 |-  ( ( A C_ y /\ Tr y ) -> Tr y )
5 3 4 mpgbir 
 |-  A. x e. { y | ( A C_ y /\ Tr y ) } Tr x
6 trint 
 |-  ( A. x e. { y | ( A C_ y /\ Tr y ) } Tr x -> Tr |^| { y | ( A C_ y /\ Tr y ) } )
7 5 6 ax-mp 
 |-  Tr |^| { y | ( A C_ y /\ Tr y ) }
8 ttcmin 
 |-  ( ( A C_ |^| { y | ( A C_ y /\ Tr y ) } /\ Tr |^| { y | ( A C_ y /\ Tr y ) } ) -> TC+ A C_ |^| { y | ( A C_ y /\ Tr y ) } )
9 1 7 8 mp2an 
 |-  TC+ A C_ |^| { y | ( A C_ y /\ Tr y ) }
10 df-tc 
 |-  TC = ( x e. _V |-> |^| { y | ( x C_ y /\ Tr y ) } )
11 cleq1 
 |-  ( x = A -> |^| { y | ( x C_ y /\ Tr y ) } = |^| { y | ( A C_ y /\ Tr y ) } )
12 11 adantl 
 |-  ( ( TC+ A e. V /\ x = A ) -> |^| { y | ( x C_ y /\ Tr y ) } = |^| { y | ( A C_ y /\ Tr y ) } )
13 ttcexrg 
 |-  ( TC+ A e. V -> A e. _V )
14 ttcid 
 |-  A C_ TC+ A
15 ttctr 
 |-  Tr TC+ A
16 sseq2 
 |-  ( y = TC+ A -> ( A C_ y <-> A C_ TC+ A ) )
17 treq 
 |-  ( y = TC+ A -> ( Tr y <-> Tr TC+ A ) )
18 16 17 anbi12d 
 |-  ( y = TC+ A -> ( ( A C_ y /\ Tr y ) <-> ( A C_ TC+ A /\ Tr TC+ A ) ) )
19 18 spcegv 
 |-  ( TC+ A e. V -> ( ( A C_ TC+ A /\ Tr TC+ A ) -> E. y ( A C_ y /\ Tr y ) ) )
20 14 15 19 mp2ani 
 |-  ( TC+ A e. V -> E. y ( A C_ y /\ Tr y ) )
21 intexab 
 |-  ( E. y ( A C_ y /\ Tr y ) <-> |^| { y | ( A C_ y /\ Tr y ) } e. _V )
22 20 21 sylib 
 |-  ( TC+ A e. V -> |^| { y | ( A C_ y /\ Tr y ) } e. _V )
23 10 12 13 22 fvmptd2 
 |-  ( TC+ A e. V -> ( TC ` A ) = |^| { y | ( A C_ y /\ Tr y ) } )
24 9 23 sseqtrrid 
 |-  ( TC+ A e. V -> TC+ A C_ ( TC ` A ) )
25 14 15 pm3.2i 
 |-  ( A C_ TC+ A /\ Tr TC+ A )
26 18 25 intmin3 
 |-  ( TC+ A e. V -> |^| { y | ( A C_ y /\ Tr y ) } C_ TC+ A )
27 23 26 eqsstrd 
 |-  ( TC+ A e. V -> ( TC ` A ) C_ TC+ A )
28 24 27 eqssd 
 |-  ( TC+ A e. V -> TC+ A = ( TC ` A ) )