Theorem axtco

Description: Axiom of Transitive Containment, derived as a theorem from ax-ext , ax-rep , and ax-inf2 . Use ax-tco instead. (Contributed by Matthew House, 6-Apr-2026) (New usage is discouraged.)

	Ref	Expression
Assertion	axtco	$$⊢\exists y\left(x\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
2	1	tz9.1	$$⊢\exists y\left(\left\{x\right\}\subseteq y\wedge \mathrm{Tr}y\wedge \forall z\left(\left(\left\{x\right\}\subseteq z\wedge \mathrm{Tr}z\right)\to y\subseteq z\right)\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4	3	snss	$$⊢x\in y\leftrightarrow \left\{x\right\}\subseteq y$$
5		dftr3	$$⊢\mathrm{Tr}y\leftrightarrow \forall z\in yz\subseteq y$$
6		df-ss	$$⊢z\subseteq y\leftrightarrow \forall w\left(w\in z\to w\in y\right)$$
7	6	ralbii	$$⊢\forall z\in yz\subseteq y\leftrightarrow \forall z\in y\forall w\left(w\in z\to w\in y\right)$$
8		df-ral	$$⊢\forall z\in y\forall w\left(w\in z\to w\in y\right)\leftrightarrow \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)$$
9	5 7 8	3bitrri	$$⊢\forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\leftrightarrow \mathrm{Tr}y$$
10	4 9	anbi12i	$$⊢\left(x\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)\leftrightarrow \left(\left\{x\right\}\subseteq y\wedge \mathrm{Tr}y\right)$$
11	10	biimpri	$$⊢\left(\left\{x\right\}\subseteq y\wedge \mathrm{Tr}y\right)\to \left(x\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)$$
12	11	3adant3	$$⊢\left(\left\{x\right\}\subseteq y\wedge \mathrm{Tr}y\wedge \forall z\left(\left(\left\{x\right\}\subseteq z\wedge \mathrm{Tr}z\right)\to y\subseteq z\right)\right)\to \left(x\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)$$
13	2 12	eximii	$$⊢\exists y\left(x\in y\wedge \forall z\left(z\in y\to \forall w\left(w\in z\to w\in y\right)\right)\right)$$