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

Theorem iiner 7764
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 4032 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ∃𝑥𝐴 𝑅 Er 𝐵)
2 errel 7696 . . . . . 6 (𝑅 Er 𝐵 → Rel 𝑅)
3 df-rel 5081 . . . . . 6 (Rel 𝑅𝑅 ⊆ (V × V))
42, 3sylib 208 . . . . 5 (𝑅 Er 𝐵𝑅 ⊆ (V × V))
54reximi 3005 . . . 4 (∃𝑥𝐴 𝑅 Er 𝐵 → ∃𝑥𝐴 𝑅 ⊆ (V × V))
6 iinss 4537 . . . 4 (∃𝑥𝐴 𝑅 ⊆ (V × V) → 𝑥𝐴 𝑅 ⊆ (V × V))
71, 5, 63syl 18 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 ⊆ (V × V))
8 df-rel 5081 . . 3 (Rel 𝑥𝐴 𝑅 𝑥𝐴 𝑅 ⊆ (V × V))
97, 8sylibr 224 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → Rel 𝑥𝐴 𝑅)
10 id 22 . . . . . . . . 9 (𝑅 Er 𝐵𝑅 Er 𝐵)
1110ersymb 7701 . . . . . . . 8 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
1211biimpd 219 . . . . . . 7 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
13 df-br 4614 . . . . . . 7 (𝑢𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑅)
14 df-br 4614 . . . . . . 7 (𝑣𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑅)
1512, 13, 143imtr3g 284 . . . . . 6 (𝑅 Er 𝐵 → (⟨𝑢, 𝑣⟩ ∈ 𝑅 → ⟨𝑣, 𝑢⟩ ∈ 𝑅))
1615ral2imi 2942 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
1716adantl 482 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
18 df-br 4614 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅)
19 opex 4893 . . . . . 6 𝑢, 𝑣⟩ ∈ V
20 eliin 4491 . . . . . 6 (⟨𝑢, 𝑣⟩ ∈ V → (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅))
2119, 20ax-mp 5 . . . . 5 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
2218, 21bitri 264 . . . 4 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
23 df-br 4614 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
24 opex 4893 . . . . . 6 𝑣, 𝑢⟩ ∈ V
25 eliin 4491 . . . . . 6 (⟨𝑣, 𝑢⟩ ∈ V → (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
2624, 25ax-mp 5 . . . . 5 (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2723, 26bitri 264 . . . 4 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2817, 22, 273imtr4g 285 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑢))
2928imp 445 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ 𝑢 𝑥𝐴 𝑅𝑣) → 𝑣 𝑥𝐴 𝑅𝑢)
30 r19.26 3057 . . . . 5 (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
3110ertr 7702 . . . . . . . 8 (𝑅 Er 𝐵 → ((𝑢𝑅𝑣𝑣𝑅𝑤) → 𝑢𝑅𝑤))
32 df-br 4614 . . . . . . . . 9 (𝑣𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑅)
3313, 32anbi12i 732 . . . . . . . 8 ((𝑢𝑅𝑣𝑣𝑅𝑤) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅))
34 df-br 4614 . . . . . . . 8 (𝑢𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑅)
3531, 33, 343imtr3g 284 . . . . . . 7 (𝑅 Er 𝐵 → ((⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ⟨𝑢, 𝑤⟩ ∈ 𝑅))
3635ral2imi 2942 . . . . . 6 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3736adantl 482 . . . . 5 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3830, 37syl5bir 233 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
39 df-br 4614 . . . . . 6 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
40 opex 4893 . . . . . . 7 𝑣, 𝑤⟩ ∈ V
41 eliin 4491 . . . . . . 7 (⟨𝑣, 𝑤⟩ ∈ V → (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
4240, 41ax-mp 5 . . . . . 6 (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4339, 42bitri 264 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4422, 43anbi12i 732 . . . 4 ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
45 df-br 4614 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
46 opex 4893 . . . . . 6 𝑢, 𝑤⟩ ∈ V
47 eliin 4491 . . . . . 6 (⟨𝑢, 𝑤⟩ ∈ V → (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
4846, 47ax-mp 5 . . . . 5 (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
4945, 48bitri 264 . . . 4 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
5038, 44, 493imtr4g 285 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) → 𝑢 𝑥𝐴 𝑅𝑤))
5150imp 445 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤)) → 𝑢 𝑥𝐴 𝑅𝑤)
52 simpl 473 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑅 Er 𝐵)
53 simpr 477 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝐵)
5452, 53erref 7707 . . . . . . . . 9 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝑅𝑢)
55 df-br 4614 . . . . . . . . 9 (𝑢𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5654, 55sylib 208 . . . . . . . 8 ((𝑅 Er 𝐵𝑢𝐵) → ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5756expcom 451 . . . . . . 7 (𝑢𝐵 → (𝑅 Er 𝐵 → ⟨𝑢, 𝑢⟩ ∈ 𝑅))
5857ralimdv 2957 . . . . . 6 (𝑢𝐵 → (∀𝑥𝐴 𝑅 Er 𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
5958com12 32 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
6059adantl 482 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
61 r19.26 3057 . . . . . 6 (∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) ↔ (∀𝑥𝐴 𝑅 Er 𝐵 ∧ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
62 r19.2z 4032 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅)) → ∃𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅))
63 vex 3189 . . . . . . . . . . 11 𝑢 ∈ V
6463, 63opeldm 5288 . . . . . . . . . 10 (⟨𝑢, 𝑢⟩ ∈ 𝑅𝑢 ∈ dom 𝑅)
65 erdm 7697 . . . . . . . . . . . 12 (𝑅 Er 𝐵 → dom 𝑅 = 𝐵)
6665eleq2d 2684 . . . . . . . . . . 11 (𝑅 Er 𝐵 → (𝑢 ∈ dom 𝑅𝑢𝐵))
6766biimpa 501 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢 ∈ dom 𝑅) → 𝑢𝐵)
6864, 67sylan2 491 . . . . . . . . 9 ((𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵)
6968rexlimivw 3022 . . . . . . . 8 (∃𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵)
7062, 69syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅)) → 𝑢𝐵)
7170ex 450 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵))
7261, 71syl5bir 233 . . . . 5 (𝐴 ≠ ∅ → ((∀𝑥𝐴 𝑅 Er 𝐵 ∧ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵))
7372expdimp 453 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅𝑢𝐵))
7460, 73impbid 202 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
75 df-br 4614 . . . 4 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
76 opex 4893 . . . . 5 𝑢, 𝑢⟩ ∈ V
77 eliin 4491 . . . . 5 (⟨𝑢, 𝑢⟩ ∈ V → (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
7876, 77ax-mp 5 . . . 4 (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
7975, 78bitri 264 . . 3 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
8074, 79syl6bbr 278 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵𝑢 𝑥𝐴 𝑅𝑢))
819, 29, 51, 80iserd 7713 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 Er 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wcel 1987  wne 2790  wral 2907  wrex 2908  Vcvv 3186  wss 3555  c0 3891  cop 4154   ciin 4486   class class class wbr 4613   × cxp 5072  dom cdm 5074  Rel wrel 5079   Er wer 7684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-iin 4488  df-br 4614  df-opab 4674  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-er 7687
This theorem is referenced by:  riiner  7765  efger  18052
  Copyright terms: Public domain W3C validator