erinxp

Description: A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015) (Revised by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Hypotheses	erinxp.r	$⊢ φ \to R Er A$
	erinxp.a	$⊢ φ \to B \subseteq A$
Assertion	erinxp	$⊢ φ \to (R \cap (B \times B)) Er B$

Proof

Step	Hyp	Ref	Expression
1		erinxp.r	$⊢ φ \to R Er A$
2		erinxp.a	$⊢ φ \to B \subseteq A$
3		relinxp	$⊢ Rel (R \cap (B \times B))$
4	3	a1i	$⊢ φ \to Rel (R \cap (B \times B))$
5		brinxp2	$⊢ x (R \cap (B \times B)) y \leftrightarrow ((x \in B \land y \in B) \land x R y)$
6	5	bilani	$⊢ (φ \land x (R \cap (B \times B)) y) \to ((x \in B \land y \in B) \land x R y)$
7	6	simplrd	$⊢ (φ \land x (R \cap (B \times B)) y) \to y \in B$
8	6	simplld	$⊢ (φ \land x (R \cap (B \times B)) y) \to x \in B$
9	1	adantr	$⊢ (φ \land x (R \cap (B \times B)) y) \to R Er A$
10	6	simprd	$⊢ (φ \land x (R \cap (B \times B)) y) \to x R y$
11	9 10	ersym	$⊢ (φ \land x (R \cap (B \times B)) y) \to y R x$
12		brinxp2	$⊢ y (R \cap (B \times B)) x \leftrightarrow ((y \in B \land x \in B) \land y R x)$
13	7 8 11 12	syl21anbrc	$⊢ (φ \land x (R \cap (B \times B)) y) \to y (R \cap (B \times B)) x$
14	8	adantrr	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to x \in B$
15		simprr	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to y (R \cap (B \times B)) z$
16		brinxp2	$⊢ y (R \cap (B \times B)) z \leftrightarrow ((y \in B \land z \in B) \land y R z)$
17	15 16	sylib	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to ((y \in B \land z \in B) \land y R z)$
18	17	simplrd	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to z \in B$
19	1	adantr	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to R Er A$
20	10	adantrr	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to x R y$
21	17	simprd	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to y R z$
22	19 20 21	ertrd	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to x R z$
23		brinxp2	$⊢ x (R \cap (B \times B)) z \leftrightarrow ((x \in B \land z \in B) \land x R z)$
24	14 18 22 23	syl21anbrc	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to x (R \cap (B \times B)) z$
25	1	adantr	$⊢ (φ \land x \in B) \to R Er A$
26	2	sselda	$⊢ (φ \land x \in B) \to x \in A$
27	25 26	erref	$⊢ (φ \land x \in B) \to x R x$
28	27	ex	$⊢ φ \to (x \in B \to x R x)$
29	28	pm4.71rd	$⊢ φ \to (x \in B \leftrightarrow (x R x \land x \in B))$
30		brin	$⊢ x (R \cap (B \times B)) x \leftrightarrow (x R x \land x (B \times B) x)$
31		brxp	$⊢ x (B \times B) x \leftrightarrow (x \in B \land x \in B)$
32		anidm	$⊢ (x \in B \land x \in B) \leftrightarrow x \in B$
33	31 32	bitri	$⊢ x (B \times B) x \leftrightarrow x \in B$
34	33	anbi2i	$⊢ (x R x \land x (B \times B) x) \leftrightarrow (x R x \land x \in B)$
35	30 34	bitri	$⊢ x (R \cap (B \times B)) x \leftrightarrow (x R x \land x \in B)$
36	29 35	bitr4di	$⊢ φ \to (x \in B \leftrightarrow x (R \cap (B \times B)) x)$
37	4 13 24 36	iserd	$⊢ φ \to (R \cap (B \times B)) Er B$

Metamath Proof Explorer

Theorem erinxp

Proof