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 34663
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 7912 . . 3 (𝑆 Er 𝐴 → Rel 𝑆)
21adantr 472 . 2 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → Rel 𝑆)
3 prtlem18.1 . . . 4 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝐴 (𝑥𝑢𝑦𝑢)}
43relopabi 5393 . . 3 Rel
53prtlem13 34649 . . . . . 6 (𝑧 𝑤 ↔ ∃𝑣𝐴 (𝑧𝑣𝑤𝑣))
6 simpll 807 . . . . . . . . . . . . 13 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑆 Er 𝐴)
7 simprl 811 . . . . . . . . . . . . . . 15 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣𝐴)
8 ne0i 4056 . . . . . . . . . . . . . . . 16 (𝑧𝑣𝑣 ≠ ∅)
98ad2antll 767 . . . . . . . . . . . . . . 15 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 ≠ ∅)
10 eldifsn 4454 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝐴 ∖ {∅}) ↔ (𝑣𝐴𝑣 ≠ ∅))
117, 9, 10sylanbrc 701 . . . . . . . . . . . . . 14 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 ∈ (𝐴 ∖ {∅}))
12 simplr 809 . . . . . . . . . . . . . 14 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))
1311, 12eleqtrrd 2834 . . . . . . . . . . . . 13 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 ∈ ( 𝐴 / 𝑆))
14 simprr 813 . . . . . . . . . . . . 13 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑧𝑣)
15 qsel 7985 . . . . . . . . . . . . 13 ((𝑆 Er 𝐴𝑣 ∈ ( 𝐴 / 𝑆) ∧ 𝑧𝑣) → 𝑣 = [𝑧]𝑆)
166, 13, 14, 15syl3anc 1473 . . . . . . . . . . . 12 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 = [𝑧]𝑆)
1716eleq2d 2817 . . . . . . . . . . 11 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → (𝑤𝑣𝑤 ∈ [𝑧]𝑆))
18 vex 3335 . . . . . . . . . . . 12 𝑤 ∈ V
19 vex 3335 . . . . . . . . . . . 12 𝑧 ∈ V
2018, 19elec 7945 . . . . . . . . . . 11 (𝑤 ∈ [𝑧]𝑆𝑧𝑆𝑤)
2117, 20syl6bb 276 . . . . . . . . . 10 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → (𝑤𝑣𝑧𝑆𝑤))
2221anassrs 683 . . . . . . . . 9 ((((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑣𝐴) ∧ 𝑧𝑣) → (𝑤𝑣𝑧𝑆𝑤))
2322pm5.32da 676 . . . . . . . 8 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑣𝐴) → ((𝑧𝑣𝑤𝑣) ↔ (𝑧𝑣𝑧𝑆𝑤)))
2423rexbidva 3179 . . . . . . 7 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (∃𝑣𝐴 (𝑧𝑣𝑤𝑣) ↔ ∃𝑣𝐴 (𝑧𝑣𝑧𝑆𝑤)))
25 simpll 807 . . . . . . . . . . . 12 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → 𝑆 Er 𝐴)
26 simpr 479 . . . . . . . . . . . 12 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → 𝑧𝑆𝑤)
2725, 26ercl 7914 . . . . . . . . . . 11 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → 𝑧 𝐴)
28 eluni2 4584 . . . . . . . . . . 11 (𝑧 𝐴 ↔ ∃𝑣𝐴 𝑧𝑣)
2927, 28sylib 208 . . . . . . . . . 10 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → ∃𝑣𝐴 𝑧𝑣)
3029ex 449 . . . . . . . . 9 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧𝑆𝑤 → ∃𝑣𝐴 𝑧𝑣))
3130pm4.71rd 670 . . . . . . . 8 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧𝑆𝑤 ↔ (∃𝑣𝐴 𝑧𝑣𝑧𝑆𝑤)))
32 r19.41v 3219 . . . . . . . 8 (∃𝑣𝐴 (𝑧𝑣𝑧𝑆𝑤) ↔ (∃𝑣𝐴 𝑧𝑣𝑧𝑆𝑤))
3331, 32syl6bbr 278 . . . . . . 7 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧𝑆𝑤 ↔ ∃𝑣𝐴 (𝑧𝑣𝑧𝑆𝑤)))
3424, 33bitr4d 271 . . . . . 6 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (∃𝑣𝐴 (𝑧𝑣𝑤𝑣) ↔ 𝑧𝑆𝑤))
355, 34syl5bb 272 . . . . 5 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧 𝑤𝑧𝑆𝑤))
3635adantl 473 . . . 4 (((Rel ∧ Rel 𝑆) ∧ (𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))) → (𝑧 𝑤𝑧𝑆𝑤))
3736eqbrrdv2 34644 . . 3 (((Rel ∧ Rel 𝑆) ∧ (𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))) → = 𝑆)
384, 37mpanl1 718 . 2 ((Rel 𝑆 ∧ (𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))) → = 𝑆)
392, 38mpancom 706 1 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  wcel 2131  wne 2924  wrex 3043  cdif 3704  c0 4050  {csn 4313   cuni 4580   class class class wbr 4796  {copab 4856  Rel wrel 5263   Er wer 7900  [cec 7901   / cqs 7902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-sbc 3569  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4581  df-br 4797  df-opab 4857  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-er 7903  df-ec 7905  df-qs 7909
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator