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

Theorem iiner 8471
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 4406 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ∃𝑥𝐴 𝑅 Er 𝐵)
2 errel 8400 . . . . . 6 (𝑅 Er 𝐵 → Rel 𝑅)
3 df-rel 5558 . . . . . 6 (Rel 𝑅𝑅 ⊆ (V × V))
42, 3sylib 221 . . . . 5 (𝑅 Er 𝐵𝑅 ⊆ (V × V))
54reximi 3166 . . . 4 (∃𝑥𝐴 𝑅 Er 𝐵 → ∃𝑥𝐴 𝑅 ⊆ (V × V))
6 iinss 4965 . . . 4 (∃𝑥𝐴 𝑅 ⊆ (V × V) → 𝑥𝐴 𝑅 ⊆ (V × V))
71, 5, 63syl 18 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 ⊆ (V × V))
8 df-rel 5558 . . 3 (Rel 𝑥𝐴 𝑅 𝑥𝐴 𝑅 ⊆ (V × V))
97, 8sylibr 237 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → Rel 𝑥𝐴 𝑅)
10 id 22 . . . . . . . . 9 (𝑅 Er 𝐵𝑅 Er 𝐵)
1110ersymb 8405 . . . . . . . 8 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
1211biimpd 232 . . . . . . 7 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
13 df-br 5054 . . . . . . 7 (𝑢𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑅)
14 df-br 5054 . . . . . . 7 (𝑣𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑅)
1512, 13, 143imtr3g 298 . . . . . 6 (𝑅 Er 𝐵 → (⟨𝑢, 𝑣⟩ ∈ 𝑅 → ⟨𝑣, 𝑢⟩ ∈ 𝑅))
1615ral2imi 3079 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
1716adantl 485 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
18 df-br 5054 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅)
19 opex 5348 . . . . . 6 𝑢, 𝑣⟩ ∈ V
20 eliin 4909 . . . . . 6 (⟨𝑢, 𝑣⟩ ∈ V → (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅))
2119, 20ax-mp 5 . . . . 5 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
2218, 21bitri 278 . . . 4 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
23 df-br 5054 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
24 opex 5348 . . . . . 6 𝑣, 𝑢⟩ ∈ V
25 eliin 4909 . . . . . 6 (⟨𝑣, 𝑢⟩ ∈ V → (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
2624, 25ax-mp 5 . . . . 5 (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2723, 26bitri 278 . . . 4 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2817, 22, 273imtr4g 299 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑢))
2928imp 410 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ 𝑢 𝑥𝐴 𝑅𝑣) → 𝑣 𝑥𝐴 𝑅𝑢)
30 r19.26 3092 . . . . 5 (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
3110ertr 8406 . . . . . . . 8 (𝑅 Er 𝐵 → ((𝑢𝑅𝑣𝑣𝑅𝑤) → 𝑢𝑅𝑤))
32 df-br 5054 . . . . . . . . 9 (𝑣𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑅)
3313, 32anbi12i 630 . . . . . . . 8 ((𝑢𝑅𝑣𝑣𝑅𝑤) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅))
34 df-br 5054 . . . . . . . 8 (𝑢𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑅)
3531, 33, 343imtr3g 298 . . . . . . 7 (𝑅 Er 𝐵 → ((⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ⟨𝑢, 𝑤⟩ ∈ 𝑅))
3635ral2imi 3079 . . . . . 6 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3736adantl 485 . . . . 5 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3830, 37syl5bir 246 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
39 df-br 5054 . . . . . 6 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
40 opex 5348 . . . . . . 7 𝑣, 𝑤⟩ ∈ V
41 eliin 4909 . . . . . . 7 (⟨𝑣, 𝑤⟩ ∈ V → (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
4240, 41ax-mp 5 . . . . . 6 (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4339, 42bitri 278 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4422, 43anbi12i 630 . . . 4 ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
45 df-br 5054 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
46 opex 5348 . . . . . 6 𝑢, 𝑤⟩ ∈ V
47 eliin 4909 . . . . . 6 (⟨𝑢, 𝑤⟩ ∈ V → (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
4846, 47ax-mp 5 . . . . 5 (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
4945, 48bitri 278 . . . 4 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
5038, 44, 493imtr4g 299 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) → 𝑢 𝑥𝐴 𝑅𝑤))
5150imp 410 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤)) → 𝑢 𝑥𝐴 𝑅𝑤)
52 simpl 486 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑅 Er 𝐵)
53 simpr 488 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝐵)
5452, 53erref 8411 . . . . . . . . 9 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝑅𝑢)
55 df-br 5054 . . . . . . . . 9 (𝑢𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5654, 55sylib 221 . . . . . . . 8 ((𝑅 Er 𝐵𝑢𝐵) → ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5756expcom 417 . . . . . . 7 (𝑢𝐵 → (𝑅 Er 𝐵 → ⟨𝑢, 𝑢⟩ ∈ 𝑅))
5857ralimdv 3101 . . . . . 6 (𝑢𝐵 → (∀𝑥𝐴 𝑅 Er 𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
5958com12 32 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
6059adantl 485 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
61 r19.26 3092 . . . . . 6 (∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) ↔ (∀𝑥𝐴 𝑅 Er 𝐵 ∧ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
62 r19.2z 4406 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅)) → ∃𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅))
63 vex 3412 . . . . . . . . . . 11 𝑢 ∈ V
6463, 63opeldm 5776 . . . . . . . . . 10 (⟨𝑢, 𝑢⟩ ∈ 𝑅𝑢 ∈ dom 𝑅)
65 erdm 8401 . . . . . . . . . . . 12 (𝑅 Er 𝐵 → dom 𝑅 = 𝐵)
6665eleq2d 2823 . . . . . . . . . . 11 (𝑅 Er 𝐵 → (𝑢 ∈ dom 𝑅𝑢𝐵))
6766biimpa 480 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢 ∈ dom 𝑅) → 𝑢𝐵)
6864, 67sylan2 596 . . . . . . . . 9 ((𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵)
6968rexlimivw 3201 . . . . . . . 8 (∃𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵)
7062, 69syl 17 . . . . . . 7 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅)) → 𝑢𝐵)
7170ex 416 . . . . . 6 (𝐴 ≠ ∅ → (∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵))
7261, 71syl5bir 246 . . . . 5 (𝐴 ≠ ∅ → ((∀𝑥𝐴 𝑅 Er 𝐵 ∧ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵))
7372expdimp 456 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅𝑢𝐵))
7460, 73impbid 215 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
75 df-br 5054 . . . 4 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
76 opex 5348 . . . . 5 𝑢, 𝑢⟩ ∈ V
77 eliin 4909 . . . . 5 (⟨𝑢, 𝑢⟩ ∈ V → (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
7876, 77ax-mp 5 . . . 4 (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
7975, 78bitri 278 . . 3 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
8074, 79bitr4di 292 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵𝑢 𝑥𝐴 𝑅𝑢))
819, 29, 51, 80iserd 8417 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 Er 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wcel 2110  wne 2940  wral 3061  wrex 3062  Vcvv 3408  wss 3866  c0 4237  cop 4547   ciin 4905   class class class wbr 5053   × cxp 5549  dom cdm 5551  Rel wrel 5556   Er wer 8388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-iin 4907  df-br 5054  df-opab 5116  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-er 8391
This theorem is referenced by:  riiner  8472  efger  19108
  Copyright terms: Public domain W3C validator