This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 =/= (/) /\ 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 biimtrrid 
 |-  ( ( 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 biimtrrid 
 |-  ( 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 )