tcmin

Description: Defining property of the transitive closure function: it is a subset of any transitive class containing A . (Contributed by Mario Carneiro, 23-Jun-2013)

		Ref	Expression
	Assertion	tcmin	$⊢ A \in V \to ((A \subseteq B \land Tr B) \to TC (A) \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		tcvalg	$⊢ A \in V \to TC (A) = ⋂ \{x \| (A \subseteq x \land Tr x)\}$
2		fvex	$⊢ TC (A) \in V$
3	1 2	eqeltrrdi	$⊢ A \in V \to ⋂ \{x \| (A \subseteq x \land Tr x)\} \in V$
4		intexab	$⊢ \exists x (A \subseteq x \land Tr x) \leftrightarrow ⋂ \{x \| (A \subseteq x \land Tr x)\} \in V$
5	3 4	sylibr	$⊢ A \in V \to \exists x (A \subseteq x \land Tr x)$
6		ssin	$⊢ (A \subseteq x \land A \subseteq B) \leftrightarrow A \subseteq x \cap B$
7	6	biimpi	$⊢ (A \subseteq x \land A \subseteq B) \to A \subseteq x \cap B$
8		trin	$⊢ (Tr x \land Tr B) \to Tr (x \cap B)$
9	7 8	anim12i	$⊢ ((A \subseteq x \land A \subseteq B) \land (Tr x \land Tr B)) \to (A \subseteq x \cap B \land Tr (x \cap B))$
10	9	an4s	$⊢ ((A \subseteq x \land Tr x) \land (A \subseteq B \land Tr B)) \to (A \subseteq x \cap B \land Tr (x \cap B))$
11	10	expcom	$⊢ (A \subseteq B \land Tr B) \to ((A \subseteq x \land Tr x) \to (A \subseteq x \cap B \land Tr (x \cap B)))$
12		vex	$⊢ x \in V$
13	12	inex1	$⊢ x \cap B \in V$
14		sseq2	$⊢ y = x \cap B \to (A \subseteq y \leftrightarrow A \subseteq x \cap B)$
15		treq	$⊢ y = x \cap B \to (Tr y \leftrightarrow Tr (x \cap B))$
16	14 15	anbi12d	$⊢ y = x \cap B \to ((A \subseteq y \land Tr y) \leftrightarrow (A \subseteq x \cap B \land Tr (x \cap B)))$
17	13 16	elab	$⊢ x \cap B \in \{y \| (A \subseteq y \land Tr y)\} \leftrightarrow (A \subseteq x \cap B \land Tr (x \cap B))$
18		intss1	$⊢ x \cap B \in \{y \| (A \subseteq y \land Tr y)\} \to ⋂ \{y \| (A \subseteq y \land Tr y)\} \subseteq x \cap B$
19	17 18	sylbir	$⊢ (A \subseteq x \cap B \land Tr (x \cap B)) \to ⋂ \{y \| (A \subseteq y \land Tr y)\} \subseteq x \cap B$
20		inss2	$⊢ x \cap B \subseteq B$
21	19 20	sstrdi	$⊢ (A \subseteq x \cap B \land Tr (x \cap B)) \to ⋂ \{y \| (A \subseteq y \land Tr y)\} \subseteq B$
22	11 21	syl6	$⊢ (A \subseteq B \land Tr B) \to ((A \subseteq x \land Tr x) \to ⋂ \{y \| (A \subseteq y \land Tr y)\} \subseteq B)$
23	22	exlimdv	$⊢ (A \subseteq B \land Tr B) \to (\exists x (A \subseteq x \land Tr x) \to ⋂ \{y \| (A \subseteq y \land Tr y)\} \subseteq B)$
24	5 23	syl5com	$⊢ A \in V \to ((A \subseteq B \land Tr B) \to ⋂ \{y \| (A \subseteq y \land Tr y)\} \subseteq B)$
25		tcvalg	$⊢ A \in V \to TC (A) = ⋂ \{y \| (A \subseteq y \land Tr y)\}$
26	25	sseq1d	$⊢ A \in V \to (TC (A) \subseteq B \leftrightarrow ⋂ \{y \| (A \subseteq y \land Tr y)\} \subseteq B)$
27	24 26	sylibrd	$⊢ A \in V \to ((A \subseteq B \land Tr B) \to TC (A) \subseteq B)$

Metamath Proof Explorer

Theorem tcmin

Proof