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+ 𝐴 ∈ 𝑉 → TC+ 𝐴 = ( TC ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ssmin	⊢ 𝐴 ⊆ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) }
2		treq	⊢ ( 𝑥 = 𝑦 → ( Tr 𝑥 ↔ Tr 𝑦 ) )
3	2	ralab2	⊢ ( ∀ 𝑥 ∈ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } Tr 𝑥 ↔ ∀ 𝑦 ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → Tr 𝑦 ) )
4		simpr	⊢ ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → Tr 𝑦 )
5	3 4	mpgbir	⊢ ∀ 𝑥 ∈ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } Tr 𝑥
6		trint	⊢ ( ∀ 𝑥 ∈ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } Tr 𝑥 → Tr ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } )
7	5 6	ax-mp	⊢ Tr ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) }
8		ttcmin	⊢ ( ( 𝐴 ⊆ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } ∧ Tr ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } ) → TC+ 𝐴 ⊆ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } )
9	1 7 8	mp2an	⊢ TC+ 𝐴 ⊆ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) }
10		df-tc	⊢ TC = ( 𝑥 ∈ V ↦ ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) } )
11		cleq1	⊢ ( 𝑥 = 𝐴 → ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) } = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } )
12	11	adantl	⊢ ( ( TC+ 𝐴 ∈ 𝑉 ∧ 𝑥 = 𝐴 ) → ∩ { 𝑦 ∣ ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) } = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } )
13		ttcexrg	⊢ ( TC+ 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
14		ttcid	⊢ 𝐴 ⊆ TC+ 𝐴
15		ttctr	⊢ Tr TC+ 𝐴
16		sseq2	⊢ ( 𝑦 = TC+ 𝐴 → ( 𝐴 ⊆ 𝑦 ↔ 𝐴 ⊆ TC+ 𝐴 ) )
17		treq	⊢ ( 𝑦 = TC+ 𝐴 → ( Tr 𝑦 ↔ Tr TC+ 𝐴 ) )
18	16 17	anbi12d	⊢ ( 𝑦 = TC+ 𝐴 → ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) ↔ ( 𝐴 ⊆ TC+ 𝐴 ∧ Tr TC+ 𝐴 ) ) )
19	18	spcegv	⊢ ( TC+ 𝐴 ∈ 𝑉 → ( ( 𝐴 ⊆ TC+ 𝐴 ∧ Tr TC+ 𝐴 ) → ∃ 𝑦 ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) ) )
20	14 15 19	mp2ani	⊢ ( TC+ 𝐴 ∈ 𝑉 → ∃ 𝑦 ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) )
21		intexab	⊢ ( ∃ 𝑦 ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) ↔ ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } ∈ V )
22	20 21	sylib	⊢ ( TC+ 𝐴 ∈ 𝑉 → ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } ∈ V )
23	10 12 13 22	fvmptd2	⊢ ( TC+ 𝐴 ∈ 𝑉 → ( TC ‘ 𝐴 ) = ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } )
24	9 23	sseqtrrid	⊢ ( TC+ 𝐴 ∈ 𝑉 → TC+ 𝐴 ⊆ ( TC ‘ 𝐴 ) )
25	14 15	pm3.2i	⊢ ( 𝐴 ⊆ TC+ 𝐴 ∧ Tr TC+ 𝐴 )
26	18 25	intmin3	⊢ ( TC+ 𝐴 ∈ 𝑉 → ∩ { 𝑦 ∣ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) } ⊆ TC+ 𝐴 )
27	23 26	eqsstrd	⊢ ( TC+ 𝐴 ∈ 𝑉 → ( TC ‘ 𝐴 ) ⊆ TC+ 𝐴 )
28	24 27	eqssd	⊢ ( TC+ 𝐴 ∈ 𝑉 → TC+ 𝐴 = ( TC ‘ 𝐴 ) )