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	Could not format assertion : No typesetting found for |- ( TC+ A e. V -> TC+ A = ( TC ` A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ssmin	$$⊢A\subseteq \bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
2		treq	$$⊢x=y\to \left(\mathrm{Tr}x\leftrightarrow \mathrm{Tr}y\right)$$
3	2	ralab2	$$⊢\forall x\in \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\mathrm{Tr}x\leftrightarrow \forall y\left(\left(A\subseteq y\wedge \mathrm{Tr}y\right)\to \mathrm{Tr}y\right)$$
4		simpr	$$⊢\left(A\subseteq y\wedge \mathrm{Tr}y\right)\to \mathrm{Tr}y$$
5	3 4	mpgbir	$$⊢\forall x\in \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\mathrm{Tr}x$$
6		trint	$$⊢\forall x\in \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\mathrm{Tr}x\to \mathrm{Tr}\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
7	5 6	ax-mp	$$⊢\mathrm{Tr}\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
8		ttcmin	Could not format ( ( A C_ |^| { y | ( A C_ y /\ Tr y ) } /\ Tr |^| { y | ( A C_ y /\ Tr y ) } ) -> TC+ A C_ |^| { y | ( A C_ y /\ Tr y ) } ) : No typesetting found for |- ( ( A C_ |^| { y | ( A C_ y /\ Tr y ) } /\ Tr |^| { y | ( A C_ y /\ Tr y ) } ) -> TC+ A C_ |^| { y | ( A C_ y /\ Tr y ) } ) with typecode |-
9	1 7 8	mp2an	Could not format TC+ A C_ |^| { y | ( A C_ y /\ Tr y ) } : No typesetting found for |- TC+ A C_ |^| { y | ( A C_ y /\ Tr y ) } with typecode |-
10		df-tc	$$⊢\mathrm{TC}=\left(x\in \mathrm{V}⟼\bigcap \left\{y|\left(x\subseteq y\wedge \mathrm{Tr}y\right)\right\}\right)$$
11		cleq1	$$⊢x=A\to \bigcap \left\{y|\left(x\subseteq y\wedge \mathrm{Tr}y\right)\right\}=\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
12	11	adantl	Could not format ( ( TC+ A e. V /\ x = A ) -> |^| { y | ( x C_ y /\ Tr y ) } = |^| { y | ( A C_ y /\ Tr y ) } ) : No typesetting found for |- ( ( TC+ A e. V /\ x = A ) -> |^| { y | ( x C_ y /\ Tr y ) } = |^| { y | ( A C_ y /\ Tr y ) } ) with typecode |-
13		ttcexrg	Could not format ( TC+ A e. V -> A e. _V ) : No typesetting found for |- ( TC+ A e. V -> A e. _V ) with typecode |-
14		ttcid	Could not format A C_ TC+ A : No typesetting found for |- A C_ TC+ A with typecode |-
15		ttctr	Could not format Tr TC+ A : No typesetting found for |- Tr TC+ A with typecode |-
16		sseq2	Could not format ( y = TC+ A -> ( A C_ y <-> A C_ TC+ A ) ) : No typesetting found for |- ( y = TC+ A -> ( A C_ y <-> A C_ TC+ A ) ) with typecode |-
17		treq	Could not format ( y = TC+ A -> ( Tr y <-> Tr TC+ A ) ) : No typesetting found for |- ( y = TC+ A -> ( Tr y <-> Tr TC+ A ) ) with typecode |-
18	16 17	anbi12d	Could not format ( y = TC+ A -> ( ( A C_ y /\ Tr y ) <-> ( A C_ TC+ A /\ Tr TC+ A ) ) ) : No typesetting found for |- ( y = TC+ A -> ( ( A C_ y /\ Tr y ) <-> ( A C_ TC+ A /\ Tr TC+ A ) ) ) with typecode |-
19	18	spcegv	Could not format ( TC+ A e. V -> ( ( A C_ TC+ A /\ Tr TC+ A ) -> E. y ( A C_ y /\ Tr y ) ) ) : No typesetting found for |- ( TC+ A e. V -> ( ( A C_ TC+ A /\ Tr TC+ A ) -> E. y ( A C_ y /\ Tr y ) ) ) with typecode |-
20	14 15 19	mp2ani	Could not format ( TC+ A e. V -> E. y ( A C_ y /\ Tr y ) ) : No typesetting found for |- ( TC+ A e. V -> E. y ( A C_ y /\ Tr y ) ) with typecode |-
21		intexab	$$⊢\exists y\left(A\subseteq y\wedge \mathrm{Tr}y\right)\leftrightarrow \bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\in \mathrm{V}$$
22	20 21	sylib	Could not format ( TC+ A e. V -> |^| { y | ( A C_ y /\ Tr y ) } e. _V ) : No typesetting found for |- ( TC+ A e. V -> |^| { y | ( A C_ y /\ Tr y ) } e. _V ) with typecode |-
23	10 12 13 22	fvmptd2	Could not format ( TC+ A e. V -> ( TC ` A ) = |^| { y | ( A C_ y /\ Tr y ) } ) : No typesetting found for |- ( TC+ A e. V -> ( TC ` A ) = |^| { y | ( A C_ y /\ Tr y ) } ) with typecode |-
24	9 23	sseqtrrid	Could not format ( TC+ A e. V -> TC+ A C_ ( TC ` A ) ) : No typesetting found for |- ( TC+ A e. V -> TC+ A C_ ( TC ` A ) ) with typecode |-
25	14 15	pm3.2i	Could not format ( A C_ TC+ A /\ Tr TC+ A ) : No typesetting found for |- ( A C_ TC+ A /\ Tr TC+ A ) with typecode |-
26	18 25	intmin3	Could not format ( TC+ A e. V -> |^| { y | ( A C_ y /\ Tr y ) } C_ TC+ A ) : No typesetting found for |- ( TC+ A e. V -> |^| { y | ( A C_ y /\ Tr y ) } C_ TC+ A ) with typecode |-
27	23 26	eqsstrd	Could not format ( TC+ A e. V -> ( TC ` A ) C_ TC+ A ) : No typesetting found for |- ( TC+ A e. V -> ( TC ` A ) C_ TC+ A ) with typecode |-
28	24 27	eqssd	Could not format ( TC+ A e. V -> TC+ A = ( TC ` A ) ) : No typesetting found for |- ( TC+ A e. V -> TC+ A = ( TC ` A ) ) with typecode |-