MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iiner Structured version   Visualization version   GIF version

Theorem iiner 7982
Description: The intersection of a nonempty family of equivalence relations is an equivalence relation. (Contributed by Mario Carneiro, 27-Sep-2015.)
Assertion
Ref Expression
iiner ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 Er 𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝑅(𝑥)

Proof of Theorem iiner
Dummy variables 𝑣 𝑢 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r19.2z 4200 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ∃𝑥𝐴 𝑅 Er 𝐵)
2 errel 7916 . . . . . 6 (𝑅 Er 𝐵 → Rel 𝑅)
3 df-rel 5269 . . . . . 6 (Rel 𝑅𝑅 ⊆ (V × V))
42, 3sylib 208 . . . . 5 (𝑅 Er 𝐵𝑅 ⊆ (V × V))
54reximi 3145 . . . 4 (∃𝑥𝐴 𝑅 Er 𝐵 → ∃𝑥𝐴 𝑅 ⊆ (V × V))
6 iinss 4719 . . . 4 (∃𝑥𝐴 𝑅 ⊆ (V × V) → 𝑥𝐴 𝑅 ⊆ (V × V))
71, 5, 63syl 18 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 ⊆ (V × V))
8 df-rel 5269 . . 3 (Rel 𝑥𝐴 𝑅 𝑥𝐴 𝑅 ⊆ (V × V))
97, 8sylibr 224 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → Rel 𝑥𝐴 𝑅)
10 id 22 . . . . . . . . 9 (𝑅 Er 𝐵𝑅 Er 𝐵)
1110ersymb 7921 . . . . . . . 8 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
1211biimpd 219 . . . . . . 7 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
13 df-br 4801 . . . . . . 7 (𝑢𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑅)
14 df-br 4801 . . . . . . 7 (𝑣𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑅)
1512, 13, 143imtr3g 284 . . . . . 6 (𝑅 Er 𝐵 → (⟨𝑢, 𝑣⟩ ∈ 𝑅 → ⟨𝑣, 𝑢⟩ ∈ 𝑅))
1615ral2imi 3081 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
1716adantl 473 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
18 df-br 4801 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅)
19 opex 5077 . . . . . 6 𝑢, 𝑣⟩ ∈ V
20 eliin 4673 . . . . . 6 (⟨𝑢, 𝑣⟩ ∈ V → (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅))
2119, 20ax-mp 5 . . . . 5 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
2218, 21bitri 264 . . . 4 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
23 df-br 4801 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
24 opex 5077 . . . . . 6 𝑣, 𝑢⟩ ∈ V
25 eliin 4673 . . . . . 6 (⟨𝑣, 𝑢⟩ ∈ V → (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
2624, 25ax-mp 5 . . . . 5 (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2723, 26bitri 264 . . . 4 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2817, 22, 273imtr4g 285 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑢))
2928imp 444 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ 𝑢 𝑥𝐴 𝑅𝑣) → 𝑣 𝑥𝐴 𝑅𝑢)
30 r19.26 3198 . . . . 5 (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
3110ertr 7922 . . . . . . . 8 (𝑅 Er 𝐵 → ((𝑢𝑅𝑣𝑣𝑅𝑤) → 𝑢𝑅𝑤))
32 df-br 4801 . . . . . . . . 9 (𝑣𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑅)
3313, 32anbi12i 735 . . . . . . . 8 ((𝑢𝑅𝑣𝑣𝑅𝑤) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅))
34 df-br 4801 . . . . . . . 8 (𝑢𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑅)
3531, 33, 343imtr3g 284 . . . . . . 7 (𝑅 Er 𝐵 → ((⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ⟨𝑢, 𝑤⟩ ∈ 𝑅))
3635ral2imi 3081 . . . . . 6 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3736adantl 473 . . . . 5 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3830, 37syl5bir 233 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
39 df-br 4801 . . . . . 6 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
40 opex 5077 . . . . . . 7 𝑣, 𝑤⟩ ∈ V
41 eliin 4673 . . . . . . 7 (⟨𝑣, 𝑤⟩ ∈ V → (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
4240, 41ax-mp 5 . . . . . 6 (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4339, 42bitri 264 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4422, 43anbi12i 735 . . . 4 ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
45 df-br 4801 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
46 opex 5077 . . . . . 6 𝑢, 𝑤⟩ ∈ V
47 eliin 4673 . . . . . 6 (⟨𝑢, 𝑤⟩ ∈ V → (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
4846, 47ax-mp 5 . . . . 5 (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
4945, 48bitri 264 . . . 4 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
5038, 44, 493imtr4g 285 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) → 𝑢 𝑥𝐴 𝑅𝑤))
5150imp 444 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤)) → 𝑢 𝑥𝐴 𝑅𝑤)
52 simpl 474 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑅 Er 𝐵)
53 simpr 479 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝐵)
5452, 53erref 7927 . . . . . . . . 9 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝑅𝑢)
55 df-br 4801 . . . . . . . . 9 (𝑢𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5654, 55sylib 208 . . . . . . . 8 ((𝑅 Er 𝐵𝑢𝐵) → ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5756expcom 450 . . . . . . 7 (𝑢𝐵 → (𝑅 Er 𝐵 → ⟨𝑢, 𝑢⟩ ∈ 𝑅))
5857ralimdv 3097 . . . . . 6 (𝑢𝐵 → (∀𝑥𝐴 𝑅 Er 𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
5958com12 32 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
6059adantl 473 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
61 r19.26 3198 . . . . . 6 (∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) ↔ (∀𝑥𝐴 𝑅 Er 𝐵 ∧ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
62 r19.2z 4200 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅)) → ∃𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅))
63 vex 3339 . . . . . . . . . . 11 𝑢 ∈ V
6463, 63opeldm 5479 . . . . . . . . . 10 (⟨𝑢, 𝑢⟩ ∈ 𝑅𝑢 ∈ dom 𝑅)
65 erdm 7917 . . . . . . . . . . . 12 (𝑅 Er 𝐵 → dom 𝑅 = 𝐵)
6665eleq2d 2821 . . . . . . . . . . 11 (𝑅 Er 𝐵 → (𝑢 ∈ dom 𝑅𝑢𝐵))
6766biimpa 502 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢 ∈ dom 𝑅) → 𝑢𝐵)
6864, 67sylan2 492 . . . . . . . . 9 ((𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵)
6968rexlimivw 3163 . . . . . . . 8 (∃𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵)
7062, 69syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅)) → 𝑢𝐵)
7170ex 449 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵))
7261, 71syl5bir 233 . . . . 5 (𝐴 ≠ ∅ → ((∀𝑥𝐴 𝑅 Er 𝐵 ∧ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵))
7372expdimp 452 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅𝑢𝐵))
7460, 73impbid 202 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
75 df-br 4801 . . . 4 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
76 opex 5077 . . . . 5 𝑢, 𝑢⟩ ∈ V
77 eliin 4673 . . . . 5 (⟨𝑢, 𝑢⟩ ∈ V → (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
7876, 77ax-mp 5 . . . 4 (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
7975, 78bitri 264 . . 3 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
8074, 79syl6bbr 278 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵𝑢 𝑥𝐴 𝑅𝑢))
819, 29, 51, 80iserd 7933 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 Er 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2135  wne 2928  wral 3046  wrex 3047  Vcvv 3336  wss 3711  c0 4054  cop 4323   ciin 4669   class class class wbr 4800   × cxp 5260  dom cdm 5262  Rel wrel 5267   Er wer 7904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pr 5051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-rab 3055  df-v 3338  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-nul 4055  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-iin 4671  df-br 4801  df-opab 4861  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-er 7907
This theorem is referenced by:  riiner  7983  efger  18327
  Copyright terms: Public domain W3C validator