Metamath Proof Explorer


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 x A R Er B x A R Er B

Proof

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