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

Theorem iiner 7862
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 4093 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ∃𝑥𝐴 𝑅 Er 𝐵)
2 errel 7796 . . . . . 6 (𝑅 Er 𝐵 → Rel 𝑅)
3 df-rel 5150 . . . . . 6 (Rel 𝑅𝑅 ⊆ (V × V))
42, 3sylib 208 . . . . 5 (𝑅 Er 𝐵𝑅 ⊆ (V × V))
54reximi 3040 . . . 4 (∃𝑥𝐴 𝑅 Er 𝐵 → ∃𝑥𝐴 𝑅 ⊆ (V × V))
6 iinss 4603 . . . 4 (∃𝑥𝐴 𝑅 ⊆ (V × V) → 𝑥𝐴 𝑅 ⊆ (V × V))
71, 5, 63syl 18 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 ⊆ (V × V))
8 df-rel 5150 . . 3 (Rel 𝑥𝐴 𝑅 𝑥𝐴 𝑅 ⊆ (V × V))
97, 8sylibr 224 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → Rel 𝑥𝐴 𝑅)
10 id 22 . . . . . . . . 9 (𝑅 Er 𝐵𝑅 Er 𝐵)
1110ersymb 7801 . . . . . . . 8 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
1211biimpd 219 . . . . . . 7 (𝑅 Er 𝐵 → (𝑢𝑅𝑣𝑣𝑅𝑢))
13 df-br 4686 . . . . . . 7 (𝑢𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑅)
14 df-br 4686 . . . . . . 7 (𝑣𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑅)
1512, 13, 143imtr3g 284 . . . . . 6 (𝑅 Er 𝐵 → (⟨𝑢, 𝑣⟩ ∈ 𝑅 → ⟨𝑣, 𝑢⟩ ∈ 𝑅))
1615ral2imi 2976 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
1716adantl 481 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 → ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
18 df-br 4686 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅)
19 opex 4962 . . . . . 6 𝑢, 𝑣⟩ ∈ V
20 eliin 4557 . . . . . 6 (⟨𝑢, 𝑣⟩ ∈ V → (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅))
2119, 20ax-mp 5 . . . . 5 (⟨𝑢, 𝑣⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
2218, 21bitri 264 . . . 4 (𝑢 𝑥𝐴 𝑅𝑣 ↔ ∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅)
23 df-br 4686 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
24 opex 4962 . . . . . 6 𝑣, 𝑢⟩ ∈ V
25 eliin 4557 . . . . . 6 (⟨𝑣, 𝑢⟩ ∈ V → (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅))
2624, 25ax-mp 5 . . . . 5 (⟨𝑣, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2723, 26bitri 264 . . . 4 (𝑣 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑣, 𝑢⟩ ∈ 𝑅)
2817, 22, 273imtr4g 285 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑢))
2928imp 444 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ 𝑢 𝑥𝐴 𝑅𝑣) → 𝑣 𝑥𝐴 𝑅𝑢)
30 r19.26 3093 . . . . 5 (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
3110ertr 7802 . . . . . . . 8 (𝑅 Er 𝐵 → ((𝑢𝑅𝑣𝑣𝑅𝑤) → 𝑢𝑅𝑤))
32 df-br 4686 . . . . . . . . 9 (𝑣𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑅)
3313, 32anbi12i 733 . . . . . . . 8 ((𝑢𝑅𝑣𝑣𝑅𝑤) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅))
34 df-br 4686 . . . . . . . 8 (𝑢𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑅)
3531, 33, 343imtr3g 284 . . . . . . 7 (𝑅 Er 𝐵 → ((⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ⟨𝑢, 𝑤⟩ ∈ 𝑅))
3635ral2imi 2976 . . . . . 6 (∀𝑥𝐴 𝑅 Er 𝐵 → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3736adantl 481 . . . . 5 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (∀𝑥𝐴 (⟨𝑢, 𝑣⟩ ∈ 𝑅 ∧ ⟨𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
3830, 37syl5bir 233 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅) → ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
39 df-br 4686 . . . . . 6 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
40 opex 4962 . . . . . . 7 𝑣, 𝑤⟩ ∈ V
41 eliin 4557 . . . . . . 7 (⟨𝑣, 𝑤⟩ ∈ V → (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
4240, 41ax-mp 5 . . . . . 6 (⟨𝑣, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4339, 42bitri 264 . . . . 5 (𝑣 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅)
4422, 43anbi12i 733 . . . 4 ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) ↔ (∀𝑥𝐴𝑢, 𝑣⟩ ∈ 𝑅 ∧ ∀𝑥𝐴𝑣, 𝑤⟩ ∈ 𝑅))
45 df-br 4686 . . . . 5 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅)
46 opex 4962 . . . . . 6 𝑢, 𝑤⟩ ∈ V
47 eliin 4557 . . . . . 6 (⟨𝑢, 𝑤⟩ ∈ V → (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅))
4846, 47ax-mp 5 . . . . 5 (⟨𝑢, 𝑤⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
4945, 48bitri 264 . . . 4 (𝑢 𝑥𝐴 𝑅𝑤 ↔ ∀𝑥𝐴𝑢, 𝑤⟩ ∈ 𝑅)
5038, 44, 493imtr4g 285 . . 3 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → ((𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤) → 𝑢 𝑥𝐴 𝑅𝑤))
5150imp 444 . 2 (((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) ∧ (𝑢 𝑥𝐴 𝑅𝑣𝑣 𝑥𝐴 𝑅𝑤)) → 𝑢 𝑥𝐴 𝑅𝑤)
52 simpl 472 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑅 Er 𝐵)
53 simpr 476 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝐵)
5452, 53erref 7807 . . . . . . . . 9 ((𝑅 Er 𝐵𝑢𝐵) → 𝑢𝑅𝑢)
55 df-br 4686 . . . . . . . . 9 (𝑢𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5654, 55sylib 208 . . . . . . . 8 ((𝑅 Er 𝐵𝑢𝐵) → ⟨𝑢, 𝑢⟩ ∈ 𝑅)
5756expcom 450 . . . . . . 7 (𝑢𝐵 → (𝑅 Er 𝐵 → ⟨𝑢, 𝑢⟩ ∈ 𝑅))
5857ralimdv 2992 . . . . . 6 (𝑢𝐵 → (∀𝑥𝐴 𝑅 Er 𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
5958com12 32 . . . . 5 (∀𝑥𝐴 𝑅 Er 𝐵 → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
6059adantl 481 . . . 4 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵 → ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
61 r19.26 3093 . . . . . 6 (∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) ↔ (∀𝑥𝐴 𝑅 Er 𝐵 ∧ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
62 r19.2z 4093 . . . . . . . 8 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅)) → ∃𝑥𝐴 (𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅))
63 vex 3234 . . . . . . . . . . 11 𝑢 ∈ V
6463, 63opeldm 5360 . . . . . . . . . 10 (⟨𝑢, 𝑢⟩ ∈ 𝑅𝑢 ∈ dom 𝑅)
65 erdm 7797 . . . . . . . . . . . 12 (𝑅 Er 𝐵 → dom 𝑅 = 𝐵)
6665eleq2d 2716 . . . . . . . . . . 11 (𝑅 Er 𝐵 → (𝑢 ∈ dom 𝑅𝑢𝐵))
6766biimpa 500 . . . . . . . . . 10 ((𝑅 Er 𝐵𝑢 ∈ dom 𝑅) → 𝑢𝐵)
6864, 67sylan2 490 . . . . . . . . 9 ((𝑅 Er 𝐵 ∧ ⟨𝑢, 𝑢⟩ ∈ 𝑅) → 𝑢𝐵)
6968rexlimivw 3058 . . . . . . . 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 4686 . . . 4 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅)
76 opex 4962 . . . . 5 𝑢, 𝑢⟩ ∈ V
77 eliin 4557 . . . . 5 (⟨𝑢, 𝑢⟩ ∈ V → (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅))
7876, 77ax-mp 5 . . . 4 (⟨𝑢, 𝑢⟩ ∈ 𝑥𝐴 𝑅 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
7975, 78bitri 264 . . 3 (𝑢 𝑥𝐴 𝑅𝑢 ↔ ∀𝑥𝐴𝑢, 𝑢⟩ ∈ 𝑅)
8074, 79syl6bbr 278 . 2 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → (𝑢𝐵𝑢 𝑥𝐴 𝑅𝑢))
819, 29, 51, 80iserd 7813 1 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝑅 Er 𝐵) → 𝑥𝐴 𝑅 Er 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wcel 2030  wne 2823  wral 2941  wrex 2942  Vcvv 3231  wss 3607  c0 3948  cop 4216   ciin 4553   class class class wbr 4685   × cxp 5141  dom cdm 5143  Rel wrel 5148   Er wer 7784
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-iin 4555  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-er 7787
This theorem is referenced by:  riiner  7863  efger  18177
  Copyright terms: Public domain W3C validator