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 ( ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ( ( 𝐵 × 𝐵 ) ∩ ∩ 𝑥 ∈ 𝐴 𝑅 ) Er 𝐵 )

Proof

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