This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 )