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 
|- ( A. x e. A R Er B -> ( ( B X. B ) i^i |^|_ x e. A R ) Er B )

Proof

Step Hyp Ref Expression
1 xpider 
 |-  ( B X. B ) Er B
2 riin0 
 |-  ( A = (/) -> ( ( B X. B ) i^i |^|_ x e. A R ) = ( B X. B ) )
3 2 adantl 
 |-  ( ( A. x e. A R Er B /\ A = (/) ) -> ( ( B X. B ) i^i |^|_ x e. A R ) = ( B X. B ) )
4 ereq1 
 |-  ( ( ( B X. B ) i^i |^|_ x e. A R ) = ( B X. B ) -> ( ( ( B X. B ) i^i |^|_ x e. A R ) Er B <-> ( B X. B ) Er B ) )
5 3 4 syl 
 |-  ( ( A. x e. A R Er B /\ A = (/) ) -> ( ( ( B X. B ) i^i |^|_ x e. A R ) Er B <-> ( B X. B ) Er B ) )
6 1 5 mpbiri 
 |-  ( ( A. x e. A R Er B /\ A = (/) ) -> ( ( B X. B ) i^i |^|_ x e. A R ) Er B )
7 iiner 
 |-  ( ( A =/= (/) /\ A. x e. A R Er B ) -> |^|_ x e. A R Er B )
8 7 ancoms 
 |-  ( ( A. x e. A R Er B /\ A =/= (/) ) -> |^|_ x e. A R Er B )
9 erssxp 
 |-  ( R Er B -> R C_ ( B X. B ) )
10 9 ralimi 
 |-  ( A. x e. A R Er B -> A. x e. A R C_ ( B X. B ) )
11 riinn0 
 |-  ( ( A. x e. A R C_ ( B X. B ) /\ A =/= (/) ) -> ( ( B X. B ) i^i |^|_ x e. A R ) = |^|_ x e. A R )
12 10 11 sylan 
 |-  ( ( A. x e. A R Er B /\ A =/= (/) ) -> ( ( B X. B ) i^i |^|_ x e. A R ) = |^|_ x e. A R )
13 ereq1 
 |-  ( ( ( B X. B ) i^i |^|_ x e. A R ) = |^|_ x e. A R -> ( ( ( B X. B ) i^i |^|_ x e. A R ) Er B <-> |^|_ x e. A R Er B ) )
14 12 13 syl 
 |-  ( ( A. x e. A R Er B /\ A =/= (/) ) -> ( ( ( B X. B ) i^i |^|_ x e. A R ) Er B <-> |^|_ x e. A R Er B ) )
15 8 14 mpbird 
 |-  ( ( A. x e. A R Er B /\ A =/= (/) ) -> ( ( B X. B ) i^i |^|_ x e. A R ) Er B )
16 6 15 pm2.61dane 
 |-  ( A. x e. A R Er B -> ( ( B X. B ) i^i |^|_ x e. A R ) Er B )