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

Metamath Proof Explorer

Theorem riiner

Description: The relative intersection of a family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Assertion riiner ⊢ ∀ x ∈ A R Er B → B × B ∩ ⋂ x ∈ A R Er B

Proof

Step Hyp Ref Expression
1 xpider ⊢ B × B Er B
2 riin0 ⊢ A = ∅ → B × B ∩ ⋂ x ∈ A R = B × B
3 2 adantl ⊢ ∀ x ∈ A R Er B ∧ A = ∅ → B × B ∩ ⋂ x ∈ A R = B × B
4 ereq1 ⊢ B × B ∩ ⋂ x ∈ A R = B × B → B × B ∩ ⋂ x ∈ A R Er B ↔ B × B Er B
5 3 4 syl ⊢ ∀ x ∈ A R Er B ∧ A = ∅ → B × B ∩ ⋂ x ∈ A R Er B ↔ B × B Er B
6 1 5 mpbiri ⊢ ∀ x ∈ A R Er B ∧ A = ∅ → B × B ∩ ⋂ x ∈ A R Er B
7 iiner ⊢ A ≠ ∅ ∧ ∀ x ∈ A R Er B → ⋂ x ∈ A R Er B
8 7 ancoms ⊢ ∀ x ∈ A R Er B ∧ A ≠ ∅ → ⋂ x ∈ A R Er B
9 erssxp ⊢ R Er B → R ⊆ B × B
10 9 ralimi ⊢ ∀ x ∈ A R Er B → ∀ x ∈ A R ⊆ B × B
11 riinn0 ⊢ ∀ x ∈ A R ⊆ B × B ∧ A ≠ ∅ → B × B ∩ ⋂ x ∈ A R = ⋂ x ∈ A R
12 10 11 sylan ⊢ ∀ x ∈ A R Er B ∧ A ≠ ∅ → B × B ∩ ⋂ x ∈ A R = ⋂ x ∈ A R
13 ereq1 ⊢ B × B ∩ ⋂ x ∈ A R = ⋂ x ∈ A R → B × B ∩ ⋂ x ∈ A R Er B ↔ ⋂ x ∈ A R Er B
14 12 13 syl ⊢ ∀ x ∈ A R Er B ∧ A ≠ ∅ → B × B ∩ ⋂ x ∈ A R Er B ↔ ⋂ x ∈ A R Er B
15 8 14 mpbird ⊢ ∀ x ∈ A R Er B ∧ A ≠ ∅ → B × B ∩ ⋂ x ∈ A R Er B
16 6 15 pm2.61dane ⊢ ∀ x ∈ A R Er B → B × B ∩ ⋂ x ∈ A R Er B