tcel

Description: The transitive closure function converts the element relation to the subset relation. (Contributed by Mario Carneiro, 23-Jun-2013)

		Ref	Expression
	Hypothesis	tc2.1	$⊢ A \in V$
	Assertion	tcel	$⊢ B \in A \to TC (B) \subseteq TC (A)$

Step	Hyp	Ref	Expression
1		tc2.1	$⊢ A \in V$
2		tcvalg	$⊢ B \in A \to TC (B) = ⋂ \{x \| (B \subseteq x \land Tr x)\}$
3		ssel	$⊢ A \subseteq x \to (B \in A \to B \in x)$
4		trss	$⊢ Tr x \to (B \in x \to B \subseteq x)$
5	4	com12	$⊢ B \in x \to (Tr x \to B \subseteq x)$
6	3 5	syl6com	$⊢ B \in A \to (A \subseteq x \to (Tr x \to B \subseteq x))$
7	6	impd	$⊢ B \in A \to ((A \subseteq x \land Tr x) \to B \subseteq x)$
8		simpr	$⊢ (A \subseteq x \land Tr x) \to Tr x$
9	7 8	jca2	$⊢ B \in A \to ((A \subseteq x \land Tr x) \to (B \subseteq x \land Tr x))$
10	9	ss2abdv	$⊢ B \in A \to \{x \| (A \subseteq x \land Tr x)\} \subseteq \{x \| (B \subseteq x \land Tr x)\}$
11		intss	$⊢ \{x \| (A \subseteq x \land Tr x)\} \subseteq \{x \| (B \subseteq x \land Tr x)\} \to ⋂ \{x \| (B \subseteq x \land Tr x)\} \subseteq ⋂ \{x \| (A \subseteq x \land Tr x)\}$
12	10 11	syl	$⊢ B \in A \to ⋂ \{x \| (B \subseteq x \land Tr x)\} \subseteq ⋂ \{x \| (A \subseteq x \land Tr x)\}$
13		tcvalg	$⊢ A \in V \to TC (A) = ⋂ \{x \| (A \subseteq x \land Tr x)\}$
14	1 13	ax-mp	$⊢ TC (A) = ⋂ \{x \| (A \subseteq x \land Tr x)\}$
15	12 14	sseqtrrdi	$⊢ B \in A \to ⋂ \{x \| (B \subseteq x \land Tr x)\} \subseteq TC (A)$
16	2 15	eqsstrd	$⊢ B \in A \to TC (B) \subseteq TC (A)$

Metamath Proof Explorer