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