Theorem ttcexg

Description: The transitive closure of a set is a set, assuming Transitive Containment. (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Assertion	ttcexg	⊢ ( 𝐴 ∈ 𝑉 → TC+ 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		sseq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦 ) )
2	1	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) ↔ ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) ) )
3	2	exbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) ↔ ∃ 𝑦 ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) ) )
4		vex	⊢ 𝑥 ∈ V
5	4	tz9.1	⊢ ∃ 𝑦 ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ∧ ∀ 𝑧 ( ( 𝑥 ⊆ 𝑧 ∧ Tr 𝑧 ) → 𝑦 ⊆ 𝑧 ) )
6		3simpa	⊢ ( ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ∧ ∀ 𝑧 ( ( 𝑥 ⊆ 𝑧 ∧ Tr 𝑧 ) → 𝑦 ⊆ 𝑧 ) ) → ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 ) )
7	5 6	eximii	⊢ ∃ 𝑦 ( 𝑥 ⊆ 𝑦 ∧ Tr 𝑦 )
8	3 7	vtoclg	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑦 ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) )
9		ttcmin	⊢ ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → TC+ 𝐴 ⊆ 𝑦 )
10		vex	⊢ 𝑦 ∈ V
11		ssexg	⊢ ( ( TC+ 𝐴 ⊆ 𝑦 ∧ 𝑦 ∈ V ) → TC+ 𝐴 ∈ V )
12	9 10 11	sylancl	⊢ ( ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → TC+ 𝐴 ∈ V )
13	12	exlimiv	⊢ ( ∃ 𝑦 ( 𝐴 ⊆ 𝑦 ∧ Tr 𝑦 ) → TC+ 𝐴 ∈ V )
14	8 13	syl	⊢ ( 𝐴 ∈ 𝑉 → TC+ 𝐴 ∈ V )