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		simpr	$⊢ (φ \land x (R \cap (B \times B)) y) \to x (R \cap (B \times B)) y$
6		brinxp2	$⊢ x (R \cap (B \times B)) y \leftrightarrow ((x \in B \land y \in B) \land x R y)$
7	5 6	sylib	$⊢ (φ \land x (R \cap (B \times B)) y) \to ((x \in B \land y \in B) \land x R y)$
8	7	simplrd	$⊢ (φ \land x (R \cap (B \times B)) y) \to y \in B$
9	7	simplld	$⊢ (φ \land x (R \cap (B \times B)) y) \to x \in B$
10	1	adantr	$⊢ (φ \land x (R \cap (B \times B)) y) \to R Er A$
11	7	simprd	$⊢ (φ \land x (R \cap (B \times B)) y) \to x R y$
12	10 11	ersym	$⊢ (φ \land x (R \cap (B \times B)) y) \to y R x$
13		brinxp2	$⊢ y (R \cap (B \times B)) x \leftrightarrow ((y \in B \land x \in B) \land y R x)$
14	8 9 12 13	syl21anbrc	$⊢ (φ \land x (R \cap (B \times B)) y) \to y (R \cap (B \times B)) x$
15	9	adantrr	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to x \in B$
16		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$
17		brinxp2	$⊢ y (R \cap (B \times B)) z \leftrightarrow ((y \in B \land z \in B) \land y R z)$
18	16 17	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)$
19	18	simplrd	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to z \in B$
20	1	adantr	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to R Er A$
21	11	adantrr	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to x R y$
22	18	simprd	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to y R z$
23	20 21 22	ertrd	$⊢ (φ \land (x (R \cap (B \times B)) y \land y (R \cap (B \times B)) z)) \to x R z$
24		brinxp2	$⊢ x (R \cap (B \times B)) z \leftrightarrow ((x \in B \land z \in B) \land x R z)$
25	15 19 23 24	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$
26	1	adantr	$⊢ (φ \land x \in B) \to R Er A$
27	2	sselda	$⊢ (φ \land x \in B) \to x \in A$
28	26 27	erref	$⊢ (φ \land x \in B) \to x R x$
29	28	ex	$⊢ φ \to (x \in B \to x R x)$
30	29	pm4.71rd	$⊢ φ \to (x \in B \leftrightarrow (x R x \land x \in B))$
31		brin	$⊢ x (R \cap (B \times B)) x \leftrightarrow (x R x \land x (B \times B) x)$
32		brxp	$⊢ x (B \times B) x \leftrightarrow (x \in B \land x \in B)$
33		anidm	$⊢ (x \in B \land x \in B) \leftrightarrow x \in B$
34	32 33	bitri	$⊢ x (B \times B) x \leftrightarrow x \in B$
35	34	anbi2i	$⊢ (x R x \land x (B \times B) x) \leftrightarrow (x R x \land x \in B)$
36	31 35	bitri	$⊢ x (R \cap (B \times B)) x \leftrightarrow (x R x \land x \in B)$
37	30 36	bitr4di	$⊢ φ \to (x \in B \leftrightarrow x (R \cap (B \times B)) x)$
38	4 14 25 37	iserd	$⊢ φ \to (R \cap (B \times B)) Er B$

Metamath Proof Explorer

Theorem erinxp

Proof