tcss

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

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

Step	Hyp	Ref	Expression
1		tc2.1	$⊢ A \in V$
2	1	ssex	$⊢ B \subseteq A \to B \in V$
3		tcvalg	$⊢ B \in V \to TC (B) = ⋂ \{x \| (B \subseteq x \land Tr x)\}$
4	2 3	syl	$⊢ B \subseteq A \to TC (B) = ⋂ \{x \| (B \subseteq x \land Tr x)\}$
5		sstr2	$⊢ B \subseteq A \to (A \subseteq x \to B \subseteq x)$
6	5	anim1d	$⊢ B \subseteq A \to ((A \subseteq x \land Tr x) \to (B \subseteq x \land Tr x))$
7	6	ss2abdv	$⊢ B \subseteq A \to \{x \| (A \subseteq x \land Tr x)\} \subseteq \{x \| (B \subseteq x \land Tr x)\}$
8		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)\}$
9	7 8	syl	$⊢ B \subseteq A \to ⋂ \{x \| (B \subseteq x \land Tr x)\} \subseteq ⋂ \{x \| (A \subseteq x \land Tr x)\}$
10		tcvalg	$⊢ A \in V \to TC (A) = ⋂ \{x \| (A \subseteq x \land Tr x)\}$
11	1 10	ax-mp	$⊢ TC (A) = ⋂ \{x \| (A \subseteq x \land Tr x)\}$
12	9 11	sseqtrrdi	$⊢ B \subseteq A \to ⋂ \{x \| (B \subseteq x \land Tr x)\} \subseteq TC (A)$
13	4 12	eqsstrd	$⊢ B \subseteq A \to TC (B) \subseteq TC (A)$

Metamath Proof Explorer