Theorem 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	⊢ ( 𝜑 → 𝑅 Er 𝐴 )
	erinxp.a	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion	erinxp	⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) Er 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		erinxp.r	⊢ ( 𝜑 → 𝑅 Er 𝐴 )
2		erinxp.a	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
3		relinxp	⊢ Rel ( 𝑅 ∩ ( 𝐵 × 𝐵 ) )
4	3	a1i	⊢ ( 𝜑 → Rel ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) )
5		brinxp2	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) )
6	5	bilani	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) )
7	6	simplrd	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑦 ∈ 𝐵 )
8	6	simplld	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑥 ∈ 𝐵 )
9	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑅 Er 𝐴 )
10	6	simprd	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑥 𝑅 𝑦 )
11	9 10	ersym	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑦 𝑅 𝑥 )
12		brinxp2	⊢ ( 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 𝑅 𝑥 ) )
13	7 8 11 12	syl21anbrc	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 )
14	8	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑥 ∈ 𝐵 )
15		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 )
16		brinxp2	⊢ ( 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑦 𝑅 𝑧 ) )
17	15 16	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑦 𝑅 𝑧 ) )
18	17	simplrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑧 ∈ 𝐵 )
19	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑅 Er 𝐴 )
20	10	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑥 𝑅 𝑦 )
21	17	simprd	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑦 𝑅 𝑧 )
22	19 20 21	ertrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑥 𝑅 𝑧 )
23		brinxp2	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) )
24	14 18 22 23	syl21anbrc	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 )
25	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 Er 𝐴 )
26	2	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
27	25 26	erref	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 𝑅 𝑥 )
28	27	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 𝑅 𝑥 ) )
29	28	pm4.71rd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
30		brin	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 ( 𝐵 × 𝐵 ) 𝑥 ) )
31		brxp	⊢ ( 𝑥 ( 𝐵 × 𝐵 ) 𝑥 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) )
32		anidm	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐵 )
33	31 32	bitri	⊢ ( 𝑥 ( 𝐵 × 𝐵 ) 𝑥 ↔ 𝑥 ∈ 𝐵 )
34	33	anbi2i	⊢ ( ( 𝑥 𝑅 𝑥 ∧ 𝑥 ( 𝐵 × 𝐵 ) 𝑥 ) ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 ∈ 𝐵 ) )
35	30 34	bitri	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 ∈ 𝐵 ) )
36	29 35	bitr4di	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 ) )
37	4 13 24 36	iserd	⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) Er 𝐵 )