Theorem iiner

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

	Ref	Expression
Assertion	iiner	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> |^|_ x e. A R Er B )

Proof

Step	Hyp	Ref	Expression
1		r19.2z	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> E. x e. A R Er B )
2		errel	|- ( R Er B -> Rel R )
3		df-rel	|- ( Rel R <-> R C_ ( _V X. _V ) )
4	2 3	sylib	|- ( R Er B -> R C_ ( _V X. _V ) )
5	4	reximi	|- ( E. x e. A R Er B -> E. x e. A R C_ ( _V X. _V ) )
6		iinss	|- ( E. x e. A R C_ ( _V X. _V ) -> |^|_ x e. A R C_ ( _V X. _V ) )
7	1 5 6	3syl	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> |^|_ x e. A R C_ ( _V X. _V ) )
8		df-rel	|- ( Rel |^|_ x e. A R <-> |^|_ x e. A R C_ ( _V X. _V ) )
9	7 8	sylibr	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> Rel |^|_ x e. A R )
10		id	|- ( R Er B -> R Er B )
11	10	ersymb	|- ( R Er B -> ( u R v <-> v R u ) )
12	11	biimpd	|- ( R Er B -> ( u R v -> v R u ) )
13		df-br	|- ( u R v <-> <. u , v >. e. R )
14		df-br	|- ( v R u <-> <. v , u >. e. R )
15	12 13 14	3imtr3g	|- ( R Er B -> ( <. u , v >. e. R -> <. v , u >. e. R ) )
16	15	ral2imi	|- ( A. x e. A R Er B -> ( A. x e. A <. u , v >. e. R -> A. x e. A <. v , u >. e. R ) )
17	16	adantl	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> ( A. x e. A <. u , v >. e. R -> A. x e. A <. v , u >. e. R ) )
18		df-br	|- ( u |^|_ x e. A R v <-> <. u , v >. e. |^|_ x e. A R )
19		opex	|- <. u , v >. e. _V
20		eliin	|- ( <. u , v >. e. _V -> ( <. u , v >. e. |^|_ x e. A R <-> A. x e. A <. u , v >. e. R ) )
21	19 20	ax-mp	|- ( <. u , v >. e. |^|_ x e. A R <-> A. x e. A <. u , v >. e. R )
22	18 21	bitri	|- ( u |^|_ x e. A R v <-> A. x e. A <. u , v >. e. R )
23		df-br	|- ( v |^|_ x e. A R u <-> <. v , u >. e. |^|_ x e. A R )
24		opex	|- <. v , u >. e. _V
25		eliin	|- ( <. v , u >. e. _V -> ( <. v , u >. e. |^|_ x e. A R <-> A. x e. A <. v , u >. e. R ) )
26	24 25	ax-mp	|- ( <. v , u >. e. |^|_ x e. A R <-> A. x e. A <. v , u >. e. R )
27	23 26	bitri	|- ( v |^|_ x e. A R u <-> A. x e. A <. v , u >. e. R )
28	17 22 27	3imtr4g	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> ( u |^|_ x e. A R v -> v |^|_ x e. A R u ) )
29	28	imp	|- ( ( ( A =/= (/) /\ A. x e. A R Er B ) /\ u |^|_ x e. A R v ) -> v |^|_ x e. A R u )
30		r19.26	|- ( A. x e. A ( <. u , v >. e. R /\ <. v , w >. e. R ) <-> ( A. x e. A <. u , v >. e. R /\ A. x e. A <. v , w >. e. R ) )
31	10	ertr	|- ( R Er B -> ( ( u R v /\ v R w ) -> u R w ) )
32		df-br	|- ( v R w <-> <. v , w >. e. R )
33	13 32	anbi12i	|- ( ( u R v /\ v R w ) <-> ( <. u , v >. e. R /\ <. v , w >. e. R ) )
34		df-br	|- ( u R w <-> <. u , w >. e. R )
35	31 33 34	3imtr3g	|- ( R Er B -> ( ( <. u , v >. e. R /\ <. v , w >. e. R ) -> <. u , w >. e. R ) )
36	35	ral2imi	|- ( A. x e. A R Er B -> ( A. x e. A ( <. u , v >. e. R /\ <. v , w >. e. R ) -> A. x e. A <. u , w >. e. R ) )
37	36	adantl	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> ( A. x e. A ( <. u , v >. e. R /\ <. v , w >. e. R ) -> A. x e. A <. u , w >. e. R ) )
38	30 37	syl5bir	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> ( ( A. x e. A <. u , v >. e. R /\ A. x e. A <. v , w >. e. R ) -> A. x e. A <. u , w >. e. R ) )
39		df-br	|- ( v |^|_ x e. A R w <-> <. v , w >. e. |^|_ x e. A R )
40		opex	|- <. v , w >. e. _V
41		eliin	|- ( <. v , w >. e. _V -> ( <. v , w >. e. |^|_ x e. A R <-> A. x e. A <. v , w >. e. R ) )
42	40 41	ax-mp	|- ( <. v , w >. e. |^|_ x e. A R <-> A. x e. A <. v , w >. e. R )
43	39 42	bitri	|- ( v |^|_ x e. A R w <-> A. x e. A <. v , w >. e. R )
44	22 43	anbi12i	|- ( ( u |^|_ x e. A R v /\ v |^|_ x e. A R w ) <-> ( A. x e. A <. u , v >. e. R /\ A. x e. A <. v , w >. e. R ) )
45		df-br	|- ( u |^|_ x e. A R w <-> <. u , w >. e. |^|_ x e. A R )
46		opex	|- <. u , w >. e. _V
47		eliin	|- ( <. u , w >. e. _V -> ( <. u , w >. e. |^|_ x e. A R <-> A. x e. A <. u , w >. e. R ) )
48	46 47	ax-mp	|- ( <. u , w >. e. |^|_ x e. A R <-> A. x e. A <. u , w >. e. R )
49	45 48	bitri	|- ( u |^|_ x e. A R w <-> A. x e. A <. u , w >. e. R )
50	38 44 49	3imtr4g	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> ( ( u |^|_ x e. A R v /\ v |^|_ x e. A R w ) -> u |^|_ x e. A R w ) )
51	50	imp	|- ( ( ( A =/= (/) /\ A. x e. A R Er B ) /\ ( u |^|_ x e. A R v /\ v |^|_ x e. A R w ) ) -> u |^|_ x e. A R w )
52		simpl	|- ( ( R Er B /\ u e. B ) -> R Er B )
53		simpr	|- ( ( R Er B /\ u e. B ) -> u e. B )
54	52 53	erref	|- ( ( R Er B /\ u e. B ) -> u R u )
55		df-br	|- ( u R u <-> <. u , u >. e. R )
56	54 55	sylib	|- ( ( R Er B /\ u e. B ) -> <. u , u >. e. R )
57	56	expcom	|- ( u e. B -> ( R Er B -> <. u , u >. e. R ) )
58	57	ralimdv	|- ( u e. B -> ( A. x e. A R Er B -> A. x e. A <. u , u >. e. R ) )
59	58	com12	|- ( A. x e. A R Er B -> ( u e. B -> A. x e. A <. u , u >. e. R ) )
60	59	adantl	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> ( u e. B -> A. x e. A <. u , u >. e. R ) )
61		r19.26	|- ( A. x e. A ( R Er B /\ <. u , u >. e. R ) <-> ( A. x e. A R Er B /\ A. x e. A <. u , u >. e. R ) )
62		r19.2z	|- ( ( A =/= (/) /\ A. x e. A ( R Er B /\ <. u , u >. e. R ) ) -> E. x e. A ( R Er B /\ <. u , u >. e. R ) )
63		vex	|- u e. _V
64	63 63	opeldm	|- ( <. u , u >. e. R -> u e. dom R )
65		erdm	|- ( R Er B -> dom R = B )
66	65	eleq2d	|- ( R Er B -> ( u e. dom R <-> u e. B ) )
67	66	biimpa	|- ( ( R Er B /\ u e. dom R ) -> u e. B )
68	64 67	sylan2	|- ( ( R Er B /\ <. u , u >. e. R ) -> u e. B )
69	68	rexlimivw	|- ( E. x e. A ( R Er B /\ <. u , u >. e. R ) -> u e. B )
70	62 69	syl	|- ( ( A =/= (/) /\ A. x e. A ( R Er B /\ <. u , u >. e. R ) ) -> u e. B )
71	70	ex	|- ( A =/= (/) -> ( A. x e. A ( R Er B /\ <. u , u >. e. R ) -> u e. B ) )
72	61 71	syl5bir	|- ( A =/= (/) -> ( ( A. x e. A R Er B /\ A. x e. A <. u , u >. e. R ) -> u e. B ) )
73	72	expdimp	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> ( A. x e. A <. u , u >. e. R -> u e. B ) )
74	60 73	impbid	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> ( u e. B <-> A. x e. A <. u , u >. e. R ) )
75		df-br	|- ( u |^|_ x e. A R u <-> <. u , u >. e. |^|_ x e. A R )
76		opex	|- <. u , u >. e. _V
77		eliin	|- ( <. u , u >. e. _V -> ( <. u , u >. e. |^|_ x e. A R <-> A. x e. A <. u , u >. e. R ) )
78	76 77	ax-mp	|- ( <. u , u >. e. |^|_ x e. A R <-> A. x e. A <. u , u >. e. R )
79	75 78	bitri	|- ( u |^|_ x e. A R u <-> A. x e. A <. u , u >. e. R )
80	74 79	bitr4di	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> ( u e. B <-> u |^|_ x e. A R u ) )
81	9 29 51 80	iserd	|- ( ( A =/= (/) /\ A. x e. A R Er B ) -> |^|_ x e. A R Er B )