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

Proof

Step	Hyp	Ref	Expression
1		sseq1	$$⊢x=A\to \left(x\subseteq y\leftrightarrow A\subseteq y\right)$$
2	1	anbi1d	$$⊢x=A\to \left(\left(x\subseteq y\wedge \mathrm{Tr}y\right)\leftrightarrow \left(A\subseteq y\wedge \mathrm{Tr}y\right)\right)$$
3	2	exbidv	$$⊢x=A\to \left(\exists y\left(x\subseteq y\wedge \mathrm{Tr}y\right)\leftrightarrow \exists y\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right)$$
4		vex	$$⊢x\in \mathrm{V}$$
5	4	tz9.1	$$⊢\exists y\left(x\subseteq y\wedge \mathrm{Tr}y\wedge \forall z\left(\left(x\subseteq z\wedge \mathrm{Tr}z\right)\to y\subseteq z\right)\right)$$
6		3simpa	$$⊢\left(x\subseteq y\wedge \mathrm{Tr}y\wedge \forall z\left(\left(x\subseteq z\wedge \mathrm{Tr}z\right)\to y\subseteq z\right)\right)\to \left(x\subseteq y\wedge \mathrm{Tr}y\right)$$
7	5 6	eximii	$$⊢\exists y\left(x\subseteq y\wedge \mathrm{Tr}y\right)$$
8	3 7	vtoclg	$$⊢A\in V\to \exists y\left(A\subseteq y\wedge \mathrm{Tr}y\right)$$
9		ttcmin	Could not format ( ( A C_ y /\ Tr y ) -> TC+ A C_ y ) : No typesetting found for |- ( ( A C_ y /\ Tr y ) -> TC+ A C_ y ) with typecode |-
10		vex	$$⊢y\in \mathrm{V}$$
11		ssexg	Could not format ( ( TC+ A C_ y /\ y e. _V ) -> TC+ A e. _V ) : No typesetting found for |- ( ( TC+ A C_ y /\ y e. _V ) -> TC+ A e. _V ) with typecode |-
12	9 10 11	sylancl	Could not format ( ( A C_ y /\ Tr y ) -> TC+ A e. _V ) : No typesetting found for |- ( ( A C_ y /\ Tr y ) -> TC+ A e. _V ) with typecode |-
13	12	exlimiv	Could not format ( E. y ( A C_ y /\ Tr y ) -> TC+ A e. _V ) : No typesetting found for |- ( E. y ( A C_ y /\ Tr y ) -> TC+ A e. _V ) with typecode |-
14	8 13	syl	Could not format ( A e. V -> TC+ A e. _V ) : No typesetting found for |- ( A e. V -> TC+ A e. _V ) with typecode |-