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 )