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

Theorem iiner 8828
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 4501 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ∃𝑥𝐴 𝑅 Er 𝐵)
2 errel 8753 . . . . . 6 (𝑅 Er 𝐵 → Rel 𝑅)
3 df-rel 5696 . . . . . 6 (Rel 𝑅𝑅 ⊆ (V × V))
42, 3sylib 218 . . . . 5 (𝑅 Er 𝐵𝑅 ⊆ (V × V))
54reximi 3082 . . . 4 (∃𝑥𝐴 𝑅 Er 𝐵 → ∃𝑥𝐴 𝑅 ⊆ (V × V))
6 iinss 5061 . . . 4 (∃𝑥𝐴 𝑅 ⊆ (V × V) → 𝑥𝐴 𝑅 ⊆ (V × V))
71, 5, 63syl 18 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 ⊆ (V × V))
8 df-rel 5696 . . 3 (Rel 𝑥𝐴 𝑅 𝑥𝐴 𝑅 ⊆ (V × V))
97, 8sylibr 234 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → Rel 𝑥𝐴 𝑅)
10 id 22 . . . . . . . . 9 (𝑅 Er 𝐵𝑅 Er 𝐵)
1110ersymb 8758 . . . . . . . 8 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
1211biimpd 229 . . . . . . 7 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
13 df-br 5149 . . . . . . 7 (𝑢𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑅)
14 df-br 5149 . . . . . . 7 (𝑣𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑅)
1512, 13, 143imtr3g 295 . . . . . 6 (𝑅 Er 𝐵 → (⟨𝑢, 𝑣⟩ ∈ 𝑅 → ⟨𝑣, 𝑢⟩ ∈ 𝑅))
1615ral2imi 3083 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
1716adantl 481 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
18 df-br 5149 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅)
19 opex 5475 . . . . . 6 𝑢, 𝑣⟩ ∈ V
20 eliin 5001 . . . . . 6 (⟨𝑢, 𝑣⟩ ∈ V → (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅))
2119, 20ax-mp 5 . . . . 5 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
2218, 21bitri 275 . . . 4 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
23 df-br 5149 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
24 opex 5475 . . . . . 6 𝑣, 𝑢⟩ ∈ V
25 eliin 5001 . . . . . 6 (⟨𝑣, 𝑢⟩ ∈ V → (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
2624, 25ax-mp 5 . . . . 5 (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2723, 26bitri 275 . . . 4 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2817, 22, 273imtr4g 296 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑢))
2928imp 406 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ 𝑢 𝑥𝐴 𝑅𝑣) → 𝑣 𝑥𝐴 𝑅𝑢)
30 r19.26 3109 . . . . 5 (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
3110ertr 8759 . . . . . . . 8 (𝑅 Er 𝐵 → ((𝑢𝑅𝑣𝑣𝑅𝑤) → 𝑢𝑅𝑤))
32 df-br 5149 . . . . . . . . 9 (𝑣𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑅)
3313, 32anbi12i 628 . . . . . . . 8 ((𝑢𝑅𝑣𝑣𝑅𝑤) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅))
34 df-br 5149 . . . . . . . 8 (𝑢𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑅)
3531, 33, 343imtr3g 295 . . . . . . 7 (𝑅 Er 𝐵 → ((⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ⟨𝑢, 𝑤⟩ ∈ 𝑅))
3635ral2imi 3083 . . . . . 6 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3736adantl 481 . . . . 5 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3830, 37biimtrrid 243 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
39 df-br 5149 . . . . . 6 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
40 opex 5475 . . . . . . 7 𝑣, 𝑤⟩ ∈ V
41 eliin 5001 . . . . . . 7 (⟨𝑣, 𝑤⟩ ∈ V → (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
4240, 41ax-mp 5 . . . . . 6 (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4339, 42bitri 275 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4422, 43anbi12i 628 . . . 4 ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
45 df-br 5149 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
46 opex 5475 . . . . . 6 𝑢, 𝑤⟩ ∈ V
47 eliin 5001 . . . . . 6 (⟨𝑢, 𝑤⟩ ∈ V → (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
4846, 47ax-mp 5 . . . . 5 (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
4945, 48bitri 275 . . . 4 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
5038, 44, 493imtr4g 296 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) → 𝑢 𝑥𝐴 𝑅𝑤))
5150imp 406 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤)) → 𝑢 𝑥𝐴 𝑅𝑤)
52 simpl 482 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑅 Er 𝐵)
53 simpr 484 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝐵)
5452, 53erref 8764 . . . . . . . . 9 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝑅𝑢)
55 df-br 5149 . . . . . . . . 9 (𝑢𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5654, 55sylib 218 . . . . . . . 8 ((𝑅 Er 𝐵𝑢𝐵) → ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5756expcom 413 . . . . . . 7 (𝑢𝐵 → (𝑅 Er 𝐵 → ⟨𝑢, 𝑢⟩ ∈ 𝑅))
5857ralimdv 3167 . . . . . 6 (𝑢𝐵 → (∀𝑥𝐴 𝑅 Er 𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
5958com12 32 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
6059adantl 481 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
61 r19.26 3109 . . . . . 6 (∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) ↔ (∀𝑥𝐴 𝑅 Er 𝐵 ∧ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
62 r19.2z 4501 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅)) → ∃𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅))
63 vex 3482 . . . . . . . . . . 11 𝑢 ∈ V
6463, 63opeldm 5921 . . . . . . . . . 10 (⟨𝑢, 𝑢⟩ ∈ 𝑅𝑢 ∈ dom 𝑅)
65 erdm 8754 . . . . . . . . . . . 12 (𝑅 Er 𝐵 → dom 𝑅 = 𝐵)
6665eleq2d 2825 . . . . . . . . . . 11 (𝑅 Er 𝐵 → (𝑢 ∈ dom 𝑅𝑢𝐵))
6766biimpa 476 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢 ∈ dom 𝑅) → 𝑢𝐵)
6864, 67sylan2 593 . . . . . . . . 9 ((𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵)
6968rexlimivw 3149 . . . . . . . 8 (∃𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵)
7062, 69syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅)) → 𝑢𝐵)
7170ex 412 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵))
7261, 71biimtrrid 243 . . . . 5 (𝐴 ≠ ∅ → ((∀𝑥𝐴 𝑅 Er 𝐵 ∧ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵))
7372expdimp 452 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅𝑢𝐵))
7460, 73impbid 212 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
75 df-br 5149 . . . 4 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
76 opex 5475 . . . . 5 𝑢, 𝑢⟩ ∈ V
77 eliin 5001 . . . . 5 (⟨𝑢, 𝑢⟩ ∈ V → (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
7876, 77ax-mp 5 . . . 4 (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
7975, 78bitri 275 . . 3 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
8074, 79bitr4di 289 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵𝑢 𝑥𝐴 𝑅𝑢))
819, 29, 51, 80iserd 8770 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 Er 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wcel 2106  wne 2938  wral 3059  wrex 3068  Vcvv 3478  wss 3963  c0 4339  cop 4637   ciin 4997   class class class wbr 5148   × cxp 5687  dom cdm 5689  Rel wrel 5694   Er wer 8741
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-iin 4999  df-br 5149  df-opab 5211  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-er 8744
This theorem is referenced by:  riiner  8829  efger  19751
  Copyright terms: Public domain W3C validator