Mathbox for Peter Mazsa < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  erim2 Structured version   Visualization version   GIF version

Theorem erim2 36387
 Description: Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 36494 in a more convenient form , see also erim 36388). (Contributed by Rodolfo Medina, 19-Oct-2010.) (Proof shortened by Mario Carneiro, 12-Aug-2015.) (Revised by Peter Mazsa, 29-Dec-2021.)
Assertion
Ref Expression
erim2 (𝑅𝑉 → (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ∼ 𝐴 = 𝑅))

Proof of Theorem erim2
Dummy variables 𝑢 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relcoels 36145 . . . 4 Rel ∼ 𝐴
21a1i 11 . . 3 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → Rel ∼ 𝐴)
3 eqvrelrel 36308 . . . 4 ( EqvRel 𝑅 → Rel 𝑅)
43ad2antrl 727 . . 3 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → Rel 𝑅)
5 brcoels 36156 . . . . 5 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥𝐴𝑦 ↔ ∃𝑢𝐴 (𝑥𝑢𝑦𝑢)))
65el2v 3418 . . . 4 (𝑥𝐴𝑦 ↔ ∃𝑢𝐴 (𝑥𝑢𝑦𝑢))
7 simpll 766 . . . . . . . . . . . 12 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → EqvRel 𝑅)
8 simprl 770 . . . . . . . . . . . . 13 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → 𝑢𝐴)
9 simplr 768 . . . . . . . . . . . . 13 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → (dom 𝑅 / 𝑅) = 𝐴)
108, 9eleqtrrd 2856 . . . . . . . . . . . 12 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → 𝑢 ∈ (dom 𝑅 / 𝑅))
11 simprr 772 . . . . . . . . . . . 12 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → 𝑥𝑢)
12 eqvrelqsel 36327 . . . . . . . . . . . 12 (( EqvRel 𝑅𝑢 ∈ (dom 𝑅 / 𝑅) ∧ 𝑥𝑢) → 𝑢 = [𝑥]𝑅)
137, 10, 11, 12syl3anc 1369 . . . . . . . . . . 11 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → 𝑢 = [𝑥]𝑅)
1413eleq2d 2838 . . . . . . . . . 10 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → (𝑦𝑢𝑦 ∈ [𝑥]𝑅))
15 elecALTV 36003 . . . . . . . . . . 11 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑦 ∈ [𝑥]𝑅𝑥𝑅𝑦))
1615el2v 3418 . . . . . . . . . 10 (𝑦 ∈ [𝑥]𝑅𝑥𝑅𝑦)
1714, 16bitrdi 290 . . . . . . . . 9 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → (𝑦𝑢𝑥𝑅𝑦))
1817anassrs 471 . . . . . . . 8 (((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑢𝐴) ∧ 𝑥𝑢) → (𝑦𝑢𝑥𝑅𝑦))
1918pm5.32da 582 . . . . . . 7 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑢𝐴) → ((𝑥𝑢𝑦𝑢) ↔ (𝑥𝑢𝑥𝑅𝑦)))
2019rexbidva 3221 . . . . . 6 (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → (∃𝑢𝐴 (𝑥𝑢𝑦𝑢) ↔ ∃𝑢𝐴 (𝑥𝑢𝑥𝑅𝑦)))
2120adantl 485 . . . . 5 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (∃𝑢𝐴 (𝑥𝑢𝑦𝑢) ↔ ∃𝑢𝐴 (𝑥𝑢𝑥𝑅𝑦)))
22 simpll 766 . . . . . . . . . . 11 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑥𝑅𝑦) → EqvRel 𝑅)
23 simpr 488 . . . . . . . . . . 11 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑥𝑅𝑦) → 𝑥𝑅𝑦)
2422, 23eqvrelcl 36323 . . . . . . . . . 10 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑥𝑅𝑦) → 𝑥 ∈ dom 𝑅)
2524adantll 713 . . . . . . . . 9 (((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) ∧ 𝑥𝑅𝑦) → 𝑥 ∈ dom 𝑅)
26 eqvrelim 36312 . . . . . . . . . . . . . 14 ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅)
2726ad2antrl 727 . . . . . . . . . . . . 13 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → dom 𝑅 = ran 𝑅)
2827eleq2d 2838 . . . . . . . . . . . 12 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥 ∈ dom 𝑅𝑥 ∈ ran 𝑅))
29 dmqseqim2 36367 . . . . . . . . . . . . . 14 (𝑅𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝑥 ∈ ran 𝑅𝑥 𝐴))))
303, 29syl5 34 . . . . . . . . . . . . 13 (𝑅𝑉 → ( EqvRel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝑥 ∈ ran 𝑅𝑥 𝐴))))
3130imp32 422 . . . . . . . . . . . 12 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥 ∈ ran 𝑅𝑥 𝐴))
3228, 31bitrd 282 . . . . . . . . . . 11 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥 ∈ dom 𝑅𝑥 𝐴))
33 eluni2 4806 . . . . . . . . . . 11 (𝑥 𝐴 ↔ ∃𝑢𝐴 𝑥𝑢)
3432, 33bitrdi 290 . . . . . . . . . 10 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥 ∈ dom 𝑅 ↔ ∃𝑢𝐴 𝑥𝑢))
3534adantr 484 . . . . . . . . 9 (((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) ∧ 𝑥𝑅𝑦) → (𝑥 ∈ dom 𝑅 ↔ ∃𝑢𝐴 𝑥𝑢))
3625, 35mpbid 235 . . . . . . . 8 (((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) ∧ 𝑥𝑅𝑦) → ∃𝑢𝐴 𝑥𝑢)
3736ex 416 . . . . . . 7 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥𝑅𝑦 → ∃𝑢𝐴 𝑥𝑢))
3837pm4.71rd 566 . . . . . 6 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥𝑅𝑦 ↔ (∃𝑢𝐴 𝑥𝑢𝑥𝑅𝑦)))
39 r19.41v 3266 . . . . . 6 (∃𝑢𝐴 (𝑥𝑢𝑥𝑅𝑦) ↔ (∃𝑢𝐴 𝑥𝑢𝑥𝑅𝑦))
4038, 39bitr4di 292 . . . . 5 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥𝑅𝑦 ↔ ∃𝑢𝐴 (𝑥𝑢𝑥𝑅𝑦)))
4121, 40bitr4d 285 . . . 4 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (∃𝑢𝐴 (𝑥𝑢𝑦𝑢) ↔ 𝑥𝑅𝑦))
426, 41syl5bb 286 . . 3 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥𝐴𝑦𝑥𝑅𝑦))
432, 4, 42eqbrrdv 5641 . 2 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → ∼ 𝐴 = 𝑅)
4443ex 416 1 (𝑅𝑉 → (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ∼ 𝐴 = 𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1539   ∈ wcel 2112  ∃wrex 3072  Vcvv 3410  ∪ cuni 4802   class class class wbr 5037  dom cdm 5529  ran crn 5530  Rel wrel 5534  [cec 8304   / cqs 8305   ∼ ccoels 35930   EqvRel weqvrel 35946 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pr 5303  ax-un 7466 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3700  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-iun 4889  df-br 5038  df-opab 5100  df-id 5435  df-eprel 5440  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-ec 8308  df-qs 8312  df-coss 36135  df-coels 36136  df-refrel 36228  df-symrel 36256  df-trrel 36286  df-eqvrel 36296 This theorem is referenced by:  erim  36388
 Copyright terms: Public domain W3C validator