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 34667
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 7995 . . 3 (𝑆 Er 𝐴 → Rel 𝑆)
21adantr 468 . 2 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → Rel 𝑆)
3 prtlem18.1 . . . 4 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝐴 (𝑥𝑢𝑦𝑢)}
43relopabi 5458 . . 3 Rel
53prtlem13 34653 . . . . . 6 (𝑧 𝑤 ↔ ∃𝑣𝐴 (𝑧𝑣𝑤𝑣))
6 simpll 774 . . . . . . . . . . . . 13 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑆 Er 𝐴)
7 simprl 778 . . . . . . . . . . . . . . 15 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣𝐴)
8 ne0i 4133 . . . . . . . . . . . . . . . 16 (𝑧𝑣𝑣 ≠ ∅)
98ad2antll 711 . . . . . . . . . . . . . . 15 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 ≠ ∅)
10 eldifsn 4519 . . . . . . . . . . . . . . 15 (𝑣 ∈ (𝐴 ∖ {∅}) ↔ (𝑣𝐴𝑣 ≠ ∅))
117, 9, 10sylanbrc 574 . . . . . . . . . . . . . 14 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 ∈ (𝐴 ∖ {∅}))
12 simplr 776 . . . . . . . . . . . . . 14 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))
1311, 12eleqtrrd 2899 . . . . . . . . . . . . 13 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 ∈ ( 𝐴 / 𝑆))
14 simprr 780 . . . . . . . . . . . . 13 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑧𝑣)
15 qsel 8068 . . . . . . . . . . . . 13 ((𝑆 Er 𝐴𝑣 ∈ ( 𝐴 / 𝑆) ∧ 𝑧𝑣) → 𝑣 = [𝑧]𝑆)
166, 13, 14, 15syl3anc 1483 . . . . . . . . . . . 12 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → 𝑣 = [𝑧]𝑆)
1716eleq2d 2882 . . . . . . . . . . 11 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → (𝑤𝑣𝑤 ∈ [𝑧]𝑆))
18 vex 3405 . . . . . . . . . . . 12 𝑤 ∈ V
19 vex 3405 . . . . . . . . . . . 12 𝑧 ∈ V
2018, 19elec 8028 . . . . . . . . . . 11 (𝑤 ∈ [𝑧]𝑆𝑧𝑆𝑤)
2117, 20syl6bb 278 . . . . . . . . . 10 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ (𝑣𝐴𝑧𝑣)) → (𝑤𝑣𝑧𝑆𝑤))
2221anassrs 455 . . . . . . . . 9 ((((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑣𝐴) ∧ 𝑧𝑣) → (𝑤𝑣𝑧𝑆𝑤))
2322pm5.32da 570 . . . . . . . 8 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑣𝐴) → ((𝑧𝑣𝑤𝑣) ↔ (𝑧𝑣𝑧𝑆𝑤)))
2423rexbidva 3248 . . . . . . 7 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (∃𝑣𝐴 (𝑧𝑣𝑤𝑣) ↔ ∃𝑣𝐴 (𝑧𝑣𝑧𝑆𝑤)))
25 simpll 774 . . . . . . . . . . . 12 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → 𝑆 Er 𝐴)
26 simpr 473 . . . . . . . . . . . 12 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → 𝑧𝑆𝑤)
2725, 26ercl 7997 . . . . . . . . . . 11 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → 𝑧 𝐴)
28 eluni2 4645 . . . . . . . . . . 11 (𝑧 𝐴 ↔ ∃𝑣𝐴 𝑧𝑣)
2927, 28sylib 209 . . . . . . . . . 10 (((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) ∧ 𝑧𝑆𝑤) → ∃𝑣𝐴 𝑧𝑣)
3029ex 399 . . . . . . . . 9 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧𝑆𝑤 → ∃𝑣𝐴 𝑧𝑣))
3130pm4.71rd 554 . . . . . . . 8 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧𝑆𝑤 ↔ (∃𝑣𝐴 𝑧𝑣𝑧𝑆𝑤)))
32 r19.41v 3288 . . . . . . . 8 (∃𝑣𝐴 (𝑧𝑣𝑧𝑆𝑤) ↔ (∃𝑣𝐴 𝑧𝑣𝑧𝑆𝑤))
3331, 32syl6bbr 280 . . . . . . 7 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧𝑆𝑤 ↔ ∃𝑣𝐴 (𝑧𝑣𝑧𝑆𝑤)))
3424, 33bitr4d 273 . . . . . 6 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (∃𝑣𝐴 (𝑧𝑣𝑤𝑣) ↔ 𝑧𝑆𝑤))
355, 34syl5bb 274 . . . . 5 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → (𝑧 𝑤𝑧𝑆𝑤))
3635adantl 469 . . . 4 (((Rel ∧ Rel 𝑆) ∧ (𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))) → (𝑧 𝑤𝑧𝑆𝑤))
3736eqbrrdv2 34648 . . 3 (((Rel ∧ Rel 𝑆) ∧ (𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))) → = 𝑆)
384, 37mpanl1 683 . 2 ((Rel 𝑆 ∧ (𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅}))) → = 𝑆)
392, 38mpancom 671 1 ((𝑆 Er 𝐴 ∧ ( 𝐴 / 𝑆) = (𝐴 ∖ {∅})) → = 𝑆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2157  wne 2989  wrex 3108  cdif 3777  c0 4127  {csn 4381   cuni 4641   class class class wbr 4855  {copab 4917  Rel wrel 5327   Er wer 7983  [cec 7984   / cqs 7985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4986  ax-nul 4994  ax-pr 5107
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-xp 5328  df-rel 5329  df-cnv 5330  df-co 5331  df-dm 5332  df-rn 5333  df-res 5334  df-ima 5335  df-er 7986  df-ec 7988  df-qs 7992
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator