Metamath Proof Explorer

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 V$
	Assertion	tz9.1tco	$⊢ \exists x (A \subseteq x \land Tr x \land \forall y ((A \subseteq y \land Tr y) \to x \subseteq y))$

Proof

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