Metamath Proof Explorer

Theorem riiner

Description: The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015)

		Ref	Expression
	Assertion	riiner	$⊢ \forall x \in A R Er B \to ((B \times B) \cap ⋂_{x \in A} R) Er B$

Proof

Step	Hyp	Ref	Expression
1		xpider	$⊢ (B \times B) Er B$
2		riin0	$⊢ A = \emptyset \to (B \times B) \cap ⋂_{x \in A} R = B \times B$
3	2	adantl	$⊢ (\forall x \in A R Er B \land A = \emptyset) \to (B \times B) \cap ⋂_{x \in A} R = B \times B$
4		ereq1	$⊢ (B \times B) \cap ⋂_{x \in A} R = B \times B \to (((B \times B) \cap ⋂_{x \in A} R) Er B \leftrightarrow (B \times B) Er B)$
5	3 4	syl	$⊢ (\forall x \in A R Er B \land A = \emptyset) \to (((B \times B) \cap ⋂_{x \in A} R) Er B \leftrightarrow (B \times B) Er B)$
6	1 5	mpbiri	$⊢ (\forall x \in A R Er B \land A = \emptyset) \to ((B \times B) \cap ⋂_{x \in A} R) Er B$
7		iiner	$⊢ (A \neq \emptyset \land \forall x \in A R Er B) \to ⋂_{x \in A} R Er B$
8	7	ancoms	$⊢ (\forall x \in A R Er B \land A \neq \emptyset) \to ⋂_{x \in A} R Er B$
9		erssxp	$⊢ R Er B \to R \subseteq B \times B$
10	9	ralimi	$⊢ \forall x \in A R Er B \to \forall x \in A R \subseteq B \times B$
11		riinn0	$⊢ (\forall x \in A R \subseteq B \times B \land A \neq \emptyset) \to (B \times B) \cap ⋂_{x \in A} R = ⋂_{x \in A} R$
12	10 11	sylan	$⊢ (\forall x \in A R Er B \land A \neq \emptyset) \to (B \times B) \cap ⋂_{x \in A} R = ⋂_{x \in A} R$
13		ereq1	$⊢ (B \times B) \cap ⋂_{x \in A} R = ⋂_{x \in A} R \to (((B \times B) \cap ⋂_{x \in A} R) Er B \leftrightarrow ⋂_{x \in A} R Er B)$
14	12 13	syl	$⊢ (\forall x \in A R Er B \land A \neq \emptyset) \to (((B \times B) \cap ⋂_{x \in A} R) Er B \leftrightarrow ⋂_{x \in A} R Er B)$
15	8 14	mpbird	$⊢ (\forall x \in A R Er B \land A \neq \emptyset) \to ((B \times B) \cap ⋂_{x \in A} R) Er B$
16	6 15	pm2.61dane	$⊢ \forall x \in A R Er B \to ((B \times B) \cap ⋂_{x \in A} R) Er B$