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 ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 )

Proof

Step Hyp Ref Expression
1 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 )
2 errel ⊢ ( 𝑅 Er 𝐵 → Rel 𝑅 )
3 df-rel ⊢ ( Rel 𝑅 ↔ 𝑅 ⊆ ( V × V ) )
4 2 3 sylib ⊢ ( 𝑅 Er 𝐵 → 𝑅 ⊆ ( V × V ) )
5 4 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑅 ⊆ ( V × V ) )
6 iinss ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑅 ⊆ ( V × V ) → ∩ 𝑥 ∈ 𝐴 𝑅 ⊆ ( V × V ) )
7 1 5 6 3syl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ∩ 𝑥 ∈ 𝐴 𝑅 ⊆ ( V × V ) )
8 df-rel ⊢ ( Rel ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∩ 𝑥 ∈ 𝐴 𝑅 ⊆ ( V × V ) )
9 7 8 sylibr ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → Rel ∩ 𝑥 ∈ 𝐴 𝑅 )
10 id ⊢ ( 𝑅 Er 𝐵 → 𝑅 Er 𝐵 )
11 10 ersymb ⊢ ( 𝑅 Er 𝐵 → ( 𝑢 𝑅 𝑣 ↔ 𝑣 𝑅 𝑢 ) )
12 11 biimpd ⊢ ( 𝑅 Er 𝐵 → ( 𝑢 𝑅 𝑣 → 𝑣 𝑅 𝑢 ) )
13 df-br ⊢ ( 𝑢 𝑅 𝑣 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 )
14 df-br ⊢ ( 𝑣 𝑅 𝑢 ↔ ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝑅 )
15 12 13 14 3imtr3g ⊢ ( 𝑅 Er 𝐵 → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 → ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝑅 ) )
16 15 ral2imi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 → ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝑅 ) )
17 16 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 → ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝑅 ) )
18 df-br ⊢ ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑣 ↔ ⟨ 𝑢 , 𝑣 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 )
19 opex ⊢ ⟨ 𝑢 , 𝑣 ⟩ ∈ V
20 eliin ⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ V → ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 ) )
21 19 20 ax-mp ⊢ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 )
22 18 21 bitri ⊢ ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑣 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 )
23 df-br ⊢ ( 𝑣 ∩ 𝑥 ∈ 𝐴 𝑅 𝑢 ↔ ⟨ 𝑣 , 𝑢 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 )
24 opex ⊢ ⟨ 𝑣 , 𝑢 ⟩ ∈ V
25 eliin ⊢ ( ⟨ 𝑣 , 𝑢 ⟩ ∈ V → ( ⟨ 𝑣 , 𝑢 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝑅 ) )
26 24 25 ax-mp ⊢ ( ⟨ 𝑣 , 𝑢 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝑅 )
27 23 26 bitri ⊢ ( 𝑣 ∩ 𝑥 ∈ 𝐴 𝑅 𝑢 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑢 ⟩ ∈ 𝑅 )
28 17 22 27 3imtr4g ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑣 → 𝑣 ∩ 𝑥 ∈ 𝐴 𝑅 𝑢 ) )
29 28 imp ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) ∧ 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑣 ) → 𝑣 ∩ 𝑥 ∈ 𝐴 𝑅 𝑢 )
30 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 ∧ ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 ) )
31 10 ertr ⊢ ( 𝑅 Er 𝐵 → ( ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) → 𝑢 𝑅 𝑤 ) )
32 df-br ⊢ ( 𝑣 𝑅 𝑤 ↔ ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 )
33 13 32 anbi12i ⊢ ( ( 𝑢 𝑅 𝑣 ∧ 𝑣 𝑅 𝑤 ) ↔ ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 ∧ ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 ) )
34 df-br ⊢ ( 𝑢 𝑅 𝑤 ↔ ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑅 )
35 31 33 34 3imtr3g ⊢ ( 𝑅 Er 𝐵 → ( ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 ∧ ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 ) → ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑅 ) )
36 35 ral2imi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 ∧ ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 ) → ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑅 ) )
37 36 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 ∧ ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 ) → ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑅 ) )
38 30 37 syl5bir ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ( ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 ) → ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑅 ) )
39 df-br ⊢ ( 𝑣 ∩ 𝑥 ∈ 𝐴 𝑅 𝑤 ↔ ⟨ 𝑣 , 𝑤 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 )
40 opex ⊢ ⟨ 𝑣 , 𝑤 ⟩ ∈ V
41 eliin ⊢ ( ⟨ 𝑣 , 𝑤 ⟩ ∈ V → ( ⟨ 𝑣 , 𝑤 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 ) )
42 40 41 ax-mp ⊢ ( ⟨ 𝑣 , 𝑤 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 )
43 39 42 bitri ⊢ ( 𝑣 ∩ 𝑥 ∈ 𝐴 𝑅 𝑤 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 )
44 22 43 anbi12i ⊢ ( ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑣 ∧ 𝑣 ∩ 𝑥 ∈ 𝐴 𝑅 𝑤 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑣 ⟩ ∈ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑣 , 𝑤 ⟩ ∈ 𝑅 ) )
45 df-br ⊢ ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑤 ↔ ⟨ 𝑢 , 𝑤 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 )
46 opex ⊢ ⟨ 𝑢 , 𝑤 ⟩ ∈ V
47 eliin ⊢ ( ⟨ 𝑢 , 𝑤 ⟩ ∈ V → ( ⟨ 𝑢 , 𝑤 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑅 ) )
48 46 47 ax-mp ⊢ ( ⟨ 𝑢 , 𝑤 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑅 )
49 45 48 bitri ⊢ ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑤 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑤 ⟩ ∈ 𝑅 )
50 38 44 49 3imtr4g ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ( ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑣 ∧ 𝑣 ∩ 𝑥 ∈ 𝐴 𝑅 𝑤 ) → 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑤 ) )
51 50 imp ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) ∧ ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑣 ∧ 𝑣 ∩ 𝑥 ∈ 𝐴 𝑅 𝑤 ) ) → 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑤 )
52 simpl ⊢ ( ( 𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵 ) → 𝑅 Er 𝐵 )
53 simpr ⊢ ( ( 𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵 ) → 𝑢 ∈ 𝐵 )
54 52 53 erref ⊢ ( ( 𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵 ) → 𝑢 𝑅 𝑢 )
55 df-br ⊢ ( 𝑢 𝑅 𝑢 ↔ ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 )
56 54 55 sylib ⊢ ( ( 𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵 ) → ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 )
57 56 expcom ⊢ ( 𝑢 ∈ 𝐵 → ( 𝑅 Er 𝐵 → ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) )
58 57 ralimdv ⊢ ( 𝑢 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) )
59 58 com12 ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ( 𝑢 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) )
60 59 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ( 𝑢 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) )
61 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑅 Er 𝐵 ∧ ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) ↔ ( ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) )
62 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑅 Er 𝐵 ∧ ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝑅 Er 𝐵 ∧ ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) )
63 vex ⊢ 𝑢 ∈ V
64 63 63 opeldm ⊢ ( ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 → 𝑢 ∈ dom 𝑅 )
65 erdm ⊢ ( 𝑅 Er 𝐵 → dom 𝑅 = 𝐵 )
66 65 eleq2d ⊢ ( 𝑅 Er 𝐵 → ( 𝑢 ∈ dom 𝑅 ↔ 𝑢 ∈ 𝐵 ) )
67 66 biimpa ⊢ ( ( 𝑅 Er 𝐵 ∧ 𝑢 ∈ dom 𝑅 ) → 𝑢 ∈ 𝐵 )
68 64 67 sylan2 ⊢ ( ( 𝑅 Er 𝐵 ∧ ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) → 𝑢 ∈ 𝐵 )
69 68 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑅 Er 𝐵 ∧ ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) → 𝑢 ∈ 𝐵 )
70 62 69 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑅 Er 𝐵 ∧ ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) ) → 𝑢 ∈ 𝐵 )
71 70 ex ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ( 𝑅 Er 𝐵 ∧ ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) → 𝑢 ∈ 𝐵 ) )
72 61 71 syl5bir ⊢ ( 𝐴 ≠ ∅ → ( ( ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) → 𝑢 ∈ 𝐵 ) )
73 72 expdimp ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 → 𝑢 ∈ 𝐵 ) )
74 60 73 impbid ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ( 𝑢 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) )
75 df-br ⊢ ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑢 ↔ ⟨ 𝑢 , 𝑢 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 )
76 opex ⊢ ⟨ 𝑢 , 𝑢 ⟩ ∈ V
77 eliin ⊢ ( ⟨ 𝑢 , 𝑢 ⟩ ∈ V → ( ⟨ 𝑢 , 𝑢 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 ) )
78 76 77 ax-mp ⊢ ( ⟨ 𝑢 , 𝑢 ⟩ ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 )
79 75 78 bitri ⊢ ( 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑢 ↔ ∀ 𝑥 ∈ 𝐴 ⟨ 𝑢 , 𝑢 ⟩ ∈ 𝑅 )
80 74 79 bitr4di ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ( 𝑢 ∈ 𝐵 ↔ 𝑢 ∩ 𝑥 ∈ 𝐴 𝑅 𝑢 ) )
81 9 29 51 80 iserd ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 ) → ∩ 𝑥 ∈ 𝐴 𝑅 Er 𝐵 )