Theorem tz9.1tco

Description: Version of tz9.1 derived from ax-tco . (Contributed by Matthew House, 6-Apr-2026)

	Ref	Expression
Hypothesis	tz9.1tco.1	$$⊢A\in \mathrm{V}$$
Assertion	tz9.1tco	$$⊢\exists x\left(A\subseteq x\wedge \mathrm{Tr}x\wedge \forall y\left(\left(A\subseteq y\wedge \mathrm{Tr}y\right)\to x\subseteq y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tz9.1tco.1	$$⊢A\in \mathrm{V}$$
2	1	tz9.1ctco	$$⊢\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\in \mathrm{V}$$
3	2	isseti	$$⊢\exists xx=\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
4		ssmin	$$⊢A\subseteq \bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
5		sseq2	$$⊢x=\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\to \left(A\subseteq x\leftrightarrow A\subseteq \bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\right)$$
6	4 5	mpbiri	$$⊢x=\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\to A\subseteq x$$
7		treq	$$⊢z=y\to \left(\mathrm{Tr}z\leftrightarrow \mathrm{Tr}y\right)$$
8	7	ralab2	$$⊢\forall z\in \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\mathrm{Tr}z\leftrightarrow \forall y\left(\left(A\subseteq y\wedge \mathrm{Tr}y\right)\to \mathrm{Tr}y\right)$$
9		simpr	$$⊢\left(A\subseteq y\wedge \mathrm{Tr}y\right)\to \mathrm{Tr}y$$
10	8 9	mpgbir	$$⊢\forall z\in \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\mathrm{Tr}z$$
11		trint	$$⊢\forall z\in \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\mathrm{Tr}z\to \mathrm{Tr}\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
12	10 11	ax-mp	$$⊢\mathrm{Tr}\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
13		treq	$$⊢x=\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\to \left(\mathrm{Tr}x\leftrightarrow \mathrm{Tr}\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\right)$$
14	12 13	mpbiri	$$⊢x=\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\to \mathrm{Tr}x$$
15		eqimss	$$⊢x=\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\to x\subseteq \bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}$$
16		ssintab	$$⊢x\subseteq \bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\leftrightarrow \forall y\left(\left(A\subseteq y\wedge \mathrm{Tr}y\right)\to x\subseteq y\right)$$
17	15 16	sylib	$$⊢x=\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\to \forall y\left(\left(A\subseteq y\wedge \mathrm{Tr}y\right)\to x\subseteq y\right)$$
18	6 14 17	3jca	$$⊢x=\bigcap \left\{y|\left(A\subseteq y\wedge \mathrm{Tr}y\right)\right\}\to \left(A\subseteq x\wedge \mathrm{Tr}x\wedge \forall y\left(\left(A\subseteq y\wedge \mathrm{Tr}y\right)\to x\subseteq y\right)\right)$$
19	3 18	eximii	$$⊢\exists x\left(A\subseteq x\wedge \mathrm{Tr}x\wedge \forall y\left(\left(A\subseteq y\wedge \mathrm{Tr}y\right)\to x\subseteq y\right)\right)$$