trin

Description: The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994)

		Ref	Expression
	Assertion	trin	$⊢ (Tr A \land Tr B) \to Tr (A \cap B)$

Step	Hyp	Ref	Expression
1		elin	$⊢ x \in (A \cap B) \leftrightarrow (x \in A \land x \in B)$
2		trss	$⊢ Tr A \to (x \in A \to x \subseteq A)$
3		trss	$⊢ Tr B \to (x \in B \to x \subseteq B)$
4	2 3	im2anan9	$⊢ (Tr A \land Tr B) \to ((x \in A \land x \in B) \to (x \subseteq A \land x \subseteq B))$
5	1 4	biimtrid	$⊢ (Tr A \land Tr B) \to (x \in (A \cap B) \to (x \subseteq A \land x \subseteq B))$
6		ssin	$⊢ (x \subseteq A \land x \subseteq B) \leftrightarrow x \subseteq A \cap B$
7	5 6	imbitrdi	$⊢ (Tr A \land Tr B) \to (x \in (A \cap B) \to x \subseteq A \cap B)$
8	7	ralrimiv	$⊢ (Tr A \land Tr B) \to \forall x \in (A \cap B) x \subseteq A \cap B$
9		dftr3	$⊢ Tr (A \cap B) \leftrightarrow \forall x \in (A \cap B) x \subseteq A \cap B$
10	8 9	sylibr	$⊢ (Tr A \land Tr B) \to Tr (A \cap B)$

Metamath Proof Explorer