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		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 )
6		brinxp2	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) )
7	5 6	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑦 ) )
8	7	simplrd	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑦 ∈ 𝐵 )
9	7	simplld	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑥 ∈ 𝐵 )
10	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑅 Er 𝐴 )
11	7	simprd	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑥 𝑅 𝑦 )
12	10 11	ersym	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑦 𝑅 𝑥 )
13		brinxp2	⊢ ( 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 𝑅 𝑥 ) )
14	8 9 12 13	syl21anbrc	⊢ ( ( 𝜑 ∧ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ) → 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 )
15	9	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑥 ∈ 𝐵 )
16		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 )
17		brinxp2	⊢ ( 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑦 𝑅 𝑧 ) )
18	16 17	sylib	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑦 𝑅 𝑧 ) )
19	18	simplrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑧 ∈ 𝐵 )
20	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑅 Er 𝐴 )
21	11	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑥 𝑅 𝑦 )
22	18	simprd	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑦 𝑅 𝑧 )
23	20 21 22	ertrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑥 𝑅 𝑧 )
24		brinxp2	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ 𝑥 𝑅 𝑧 ) )
25	15 19 23 24	syl21anbrc	⊢ ( ( 𝜑 ∧ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑦 ∧ 𝑦 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 ) ) → 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑧 )
26	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑅 Er 𝐴 )
27	2	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
28	26 27	erref	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 𝑅 𝑥 )
29	28	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 𝑅 𝑥 ) )
30	29	pm4.71rd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
31		brin	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 ( 𝐵 × 𝐵 ) 𝑥 ) )
32		brxp	⊢ ( 𝑥 ( 𝐵 × 𝐵 ) 𝑥 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) )
33		anidm	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐵 )
34	32 33	bitri	⊢ ( 𝑥 ( 𝐵 × 𝐵 ) 𝑥 ↔ 𝑥 ∈ 𝐵 )
35	34	anbi2i	⊢ ( ( 𝑥 𝑅 𝑥 ∧ 𝑥 ( 𝐵 × 𝐵 ) 𝑥 ) ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 ∈ 𝐵 ) )
36	31 35	bitri	⊢ ( 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 ∈ 𝐵 ) )
37	30 36	bitr4di	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) 𝑥 ) )
38	4 14 25 37	iserd	⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝐵 × 𝐵 ) ) Er 𝐵 )