trin2

Description: The intersection of two transitive classes is transitive. (Contributed by FL, 31-Jul-2009)

		Ref	Expression
	Assertion	trin2	$⊢ (R \circ R \subseteq R \land S \circ S \subseteq S) \to (R \cap S) \circ (R \cap S) \subseteq R \cap S$

Proof

Step	Hyp	Ref	Expression
1		cotr	$⊢ R \circ R \subseteq R \leftrightarrow \forall x \forall y \forall z ((x R y \land y R z) \to x R z)$
2		cotr	$⊢ S \circ S \subseteq S \leftrightarrow \forall x \forall y \forall z ((x S y \land y S z) \to x S z)$
3		brin	$⊢ x (R \cap S) y \leftrightarrow (x R y \land x S y)$
4		brin	$⊢ y (R \cap S) z \leftrightarrow (y R z \land y S z)$
5		simpr	$⊢ (((x S y \land y S z) \to x S z) \land ((x R y \land y R z) \to x R z)) \to ((x R y \land y R z) \to x R z)$
6		simpl	$⊢ (((x S y \land y S z) \to x S z) \land ((x R y \land y R z) \to x R z)) \to ((x S y \land y S z) \to x S z)$
7	5 6	anim12d	$⊢ (((x S y \land y S z) \to x S z) \land ((x R y \land y R z) \to x R z)) \to (((x R y \land y R z) \land (x S y \land y S z)) \to (x R z \land x S z))$
8	7	com12	$⊢ ((x R y \land y R z) \land (x S y \land y S z)) \to ((((x S y \land y S z) \to x S z) \land ((x R y \land y R z) \to x R z)) \to (x R z \land x S z))$
9	8	an4s	$⊢ ((x R y \land x S y) \land (y R z \land y S z)) \to ((((x S y \land y S z) \to x S z) \land ((x R y \land y R z) \to x R z)) \to (x R z \land x S z))$
10	3 4 9	syl2anb	$⊢ (x (R \cap S) y \land y (R \cap S) z) \to ((((x S y \land y S z) \to x S z) \land ((x R y \land y R z) \to x R z)) \to (x R z \land x S z))$
11	10	com12	$⊢ (((x S y \land y S z) \to x S z) \land ((x R y \land y R z) \to x R z)) \to ((x (R \cap S) y \land y (R \cap S) z) \to (x R z \land x S z))$
12		brin	$⊢ x (R \cap S) z \leftrightarrow (x R z \land x S z)$
13	11 12	syl6ibr	$⊢ (((x S y \land y S z) \to x S z) \land ((x R y \land y R z) \to x R z)) \to ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z)$
14	13	alanimi	$⊢ (\forall z ((x S y \land y S z) \to x S z) \land \forall z ((x R y \land y R z) \to x R z)) \to \forall z ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z)$
15	14	alanimi	$⊢ (\forall y \forall z ((x S y \land y S z) \to x S z) \land \forall y \forall z ((x R y \land y R z) \to x R z)) \to \forall y \forall z ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z)$
16	15	alanimi	$⊢ (\forall x \forall y \forall z ((x S y \land y S z) \to x S z) \land \forall x \forall y \forall z ((x R y \land y R z) \to x R z)) \to \forall x \forall y \forall z ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z)$
17	16	ex	$⊢ \forall x \forall y \forall z ((x S y \land y S z) \to x S z) \to (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \to \forall x \forall y \forall z ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z))$
18	2 17	sylbi	$⊢ S \circ S \subseteq S \to (\forall x \forall y \forall z ((x R y \land y R z) \to x R z) \to \forall x \forall y \forall z ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z))$
19	18	com12	$⊢ \forall x \forall y \forall z ((x R y \land y R z) \to x R z) \to (S \circ S \subseteq S \to \forall x \forall y \forall z ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z))$
20	1 19	sylbi	$⊢ R \circ R \subseteq R \to (S \circ S \subseteq S \to \forall x \forall y \forall z ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z))$
21	20	imp	$⊢ (R \circ R \subseteq R \land S \circ S \subseteq S) \to \forall x \forall y \forall z ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z)$
22		cotr	$⊢ (R \cap S) \circ (R \cap S) \subseteq R \cap S \leftrightarrow \forall x \forall y \forall z ((x (R \cap S) y \land y (R \cap S) z) \to x (R \cap S) z)$
23	21 22	sylibr	$⊢ (R \circ R \subseteq R \land S \circ S \subseteq S) \to (R \cap S) \circ (R \cap S) \subseteq R \cap S$

Metamath Proof Explorer

Theorem trin2

Proof