Users' Mathboxes Mathbox for Rodolfo Medina < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  prter3 Structured version   Visualization version   GIF version

Theorem prter3 35898
Description: For every partition there exists a unique equivalence relation whose quotient set equals the partition. (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.)
Hypothesis
Ref Expression
prtlem18.1 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝐴 (𝑥𝑢𝑦𝑢)}
Assertion
Ref Expression
prter3 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → = 𝑆)
Distinct variable group:   𝑥,𝑢,𝑦,𝐴
Allowed substitution hints:   (𝑥,𝑦,𝑢)   𝑆(𝑥,𝑦,𝑢)

Proof of Theorem prter3
Dummy variables 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 errel 8287 . . 3 (𝑆 Er 𝐴 → Rel 𝑆)
21adantr 481 . 2 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → Rel 𝑆)
3 prtlem18.1 . . . 4 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝐴 (𝑥𝑢𝑦𝑢)}
43relopabi 5687 . . 3 Rel
53prtlem13 35884 . . . . . 6 (𝑧 𝑤 ↔ ∃𝑣𝐴 (𝑧𝑣𝑤𝑣))
6 simpll 763 . . . . . . . . . . . . 13 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑆 Er 𝐴)
7 simprl 767 . . . . . . . . . . . . . . 15 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣𝐴)
8 ne0i 4297 . . . . . . . . . . . . . . . 16 (𝑧𝑣𝑣 ≠ ∅)
98ad2antll 725 . . . . . . . . . . . . . . 15 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 ≠ ∅)
10 eldifsn 4711 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝐴 ∖ {∅}) ↔ (𝑣𝐴𝑣 ≠ ∅))
117, 9, 10sylanbrc 583 . . . . . . . . . . . . . 14 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 ∈ (𝐴 ∖ {∅}))
12 simplr 765 . . . . . . . . . . . . . 14 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))
1311, 12eleqtrrd 2913 . . . . . . . . . . . . 13 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 ∈ ( 𝐴 / 𝑆))
14 simprr 769 . . . . . . . . . . . . 13 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑧𝑣)
15 qsel 8365 . . . . . . . . . . . . 13 ((𝑆 Er 𝐴𝑣 ∈ ( 𝐴 / 𝑆) ∧ 𝑧𝑣) → 𝑣 = [𝑧]𝑆)
166, 13, 14, 15syl3anc 1363 . . . . . . . . . . . 12 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 = [𝑧]𝑆)
1716eleq2d 2895 . . . . . . . . . . 11 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → (𝑤𝑣𝑤 ∈ [𝑧]𝑆))
18 vex 3495 . . . . . . . . . . . 12 𝑤 ∈ V
19 vex 3495 . . . . . . . . . . . 12 𝑧 ∈ V
2018, 19elec 8322 . . . . . . . . . . 11 (𝑤 ∈ [𝑧]𝑆𝑧𝑆𝑤)
2117, 20syl6bb 288 . . . . . . . . . 10 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → (𝑤𝑣𝑧𝑆𝑤))
2221anassrs 468 . . . . . . . . 9 ((((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑣𝐴) ∧ 𝑧𝑣) → (𝑤𝑣𝑧𝑆𝑤))
2322pm5.32da 579 . . . . . . . 8 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑣𝐴) → ((𝑧𝑣𝑤𝑣) ↔ (𝑧𝑣𝑧𝑆𝑤)))
2423rexbidva 3293 . . . . . . 7 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (∃𝑣𝐴 (𝑧𝑣𝑤𝑣) ↔ ∃𝑣𝐴 (𝑧𝑣𝑧𝑆𝑤)))
25 simpll 763 . . . . . . . . . . . 12 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → 𝑆 Er 𝐴)
26 simpr 485 . . . . . . . . . . . 12 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → 𝑧𝑆𝑤)
2725, 26ercl 8289 . . . . . . . . . . 11 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → 𝑧 𝐴)
28 eluni2 4834 . . . . . . . . . . 11 (𝑧 𝐴 ↔ ∃𝑣𝐴 𝑧𝑣)
2927, 28sylib 219 . . . . . . . . . 10 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → ∃𝑣𝐴 𝑧𝑣)
3029ex 413 . . . . . . . . 9 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧𝑆𝑤 → ∃𝑣𝐴 𝑧𝑣))
3130pm4.71rd 563 . . . . . . . 8 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧𝑆𝑤 ↔ (∃𝑣𝐴 𝑧𝑣𝑧𝑆𝑤)))
32 r19.41v 3344 . . . . . . . 8 (∃𝑣𝐴 (𝑧𝑣𝑧𝑆𝑤) ↔ (∃𝑣𝐴 𝑧𝑣𝑧𝑆𝑤))
3331, 32syl6bbr 290 . . . . . . 7 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧𝑆𝑤 ↔ ∃𝑣𝐴 (𝑧𝑣𝑧𝑆𝑤)))
3424, 33bitr4d 283 . . . . . 6 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (∃𝑣𝐴 (𝑧𝑣𝑤𝑣) ↔ 𝑧𝑆𝑤))
355, 34syl5bb 284 . . . . 5 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧 𝑤𝑧𝑆𝑤))
3635adantl 482 . . . 4 (((Rel ∧ Rel 𝑆) ∧ (𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))) → (𝑧 𝑤𝑧𝑆𝑤))
3736eqbrrdv2 35879 . . 3 (((Rel ∧ Rel 𝑆) ∧ (𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))) → = 𝑆)
384, 37mpanl1 696 . 2 ((Rel 𝑆 ∧ (𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))) → = 𝑆)
392, 38mpancom 684 1 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wne 3013  wrex 3136  cdif 3930  c0 4288  {csn 4557   cuni 4830   class class class wbr 5057  {copab 5119  Rel wrel 5553   Er wer 8275  [cec 8276   / cqs 8277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-er 8278  df-ec 8280  df-qs 8284
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator