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

Theorem erim2 35442
 Description: Equivalence relation on its natural domain implies that the class of coelements on the domain is equal to the relation (this is prter3 35549 in a more convenient form , see also erim 35443). (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 35200 . . . 4 Rel ∼ 𝐴
21a1i 11 . . 3 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → Rel ∼ 𝐴)
3 eqvrelrel 35363 . . . 4 ( EqvRel 𝑅 → Rel 𝑅)
43ad2antrl 724 . . 3 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → Rel 𝑅)
5 brcoels 35211 . . . . 5 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥𝐴𝑦 ↔ ∃𝑢𝐴 (𝑥𝑢𝑦𝑢)))
65el2v 3444 . . . 4 (𝑥𝐴𝑦 ↔ ∃𝑢𝐴 (𝑥𝑢𝑦𝑢))
7 simpll 763 . . . . . . . . . . . 12 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → EqvRel 𝑅)
8 simprl 767 . . . . . . . . . . . . 13 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → 𝑢𝐴)
9 simplr 765 . . . . . . . . . . . . 13 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → (dom 𝑅 / 𝑅) = 𝐴)
108, 9eleqtrrd 2886 . . . . . . . . . . . 12 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → 𝑢 ∈ (dom 𝑅 / 𝑅))
11 simprr 769 . . . . . . . . . . . 12 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → 𝑥𝑢)
12 eqvrelqsel 35382 . . . . . . . . . . . 12 (( EqvRel 𝑅𝑢 ∈ (dom 𝑅 / 𝑅) ∧ 𝑥𝑢) → 𝑢 = [𝑥]𝑅)
137, 10, 11, 12syl3anc 1364 . . . . . . . . . . 11 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → 𝑢 = [𝑥]𝑅)
1413eleq2d 2868 . . . . . . . . . 10 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → (𝑦𝑢𝑦 ∈ [𝑥]𝑅))
15 elecALTV 35059 . . . . . . . . . . 11 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑦 ∈ [𝑥]𝑅𝑥𝑅𝑦))
1615el2v 3444 . . . . . . . . . 10 (𝑦 ∈ [𝑥]𝑅𝑥𝑅𝑦)
1714, 16syl6bb 288 . . . . . . . . 9 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ (𝑢𝐴𝑥𝑢)) → (𝑦𝑢𝑥𝑅𝑦))
1817anassrs 468 . . . . . . . 8 (((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑢𝐴) ∧ 𝑥𝑢) → (𝑦𝑢𝑥𝑅𝑦))
1918pm5.32da 579 . . . . . . 7 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑢𝐴) → ((𝑥𝑢𝑦𝑢) ↔ (𝑥𝑢𝑥𝑅𝑦)))
2019rexbidva 3259 . . . . . 6 (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → (∃𝑢𝐴 (𝑥𝑢𝑦𝑢) ↔ ∃𝑢𝐴 (𝑥𝑢𝑥𝑅𝑦)))
2120adantl 482 . . . . 5 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (∃𝑢𝐴 (𝑥𝑢𝑦𝑢) ↔ ∃𝑢𝐴 (𝑥𝑢𝑥𝑅𝑦)))
22 simpll 763 . . . . . . . . . . 11 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑥𝑅𝑦) → EqvRel 𝑅)
23 simpr 485 . . . . . . . . . . 11 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑥𝑅𝑦) → 𝑥𝑅𝑦)
2422, 23eqvrelcl 35378 . . . . . . . . . 10 ((( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) ∧ 𝑥𝑅𝑦) → 𝑥 ∈ dom 𝑅)
2524adantll 710 . . . . . . . . 9 (((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) ∧ 𝑥𝑅𝑦) → 𝑥 ∈ dom 𝑅)
26 eqvrelim 35367 . . . . . . . . . . . . . 14 ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅)
2726ad2antrl 724 . . . . . . . . . . . . 13 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → dom 𝑅 = ran 𝑅)
2827eleq2d 2868 . . . . . . . . . . . 12 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥 ∈ dom 𝑅𝑥 ∈ ran 𝑅))
29 dmqseqim2 35422 . . . . . . . . . . . . . 14 (𝑅𝑉 → (Rel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝑥 ∈ ran 𝑅𝑥 𝐴))))
303, 29syl5 34 . . . . . . . . . . . . 13 (𝑅𝑉 → ( EqvRel 𝑅 → ((dom 𝑅 / 𝑅) = 𝐴 → (𝑥 ∈ ran 𝑅𝑥 𝐴))))
3130imp32 419 . . . . . . . . . . . 12 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥 ∈ ran 𝑅𝑥 𝐴))
3228, 31bitrd 280 . . . . . . . . . . 11 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥 ∈ dom 𝑅𝑥 𝐴))
33 eluni2 4749 . . . . . . . . . . 11 (𝑥 𝐴 ↔ ∃𝑢𝐴 𝑥𝑢)
3432, 33syl6bb 288 . . . . . . . . . 10 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥 ∈ dom 𝑅 ↔ ∃𝑢𝐴 𝑥𝑢))
3534adantr 481 . . . . . . . . 9 (((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) ∧ 𝑥𝑅𝑦) → (𝑥 ∈ dom 𝑅 ↔ ∃𝑢𝐴 𝑥𝑢))
3625, 35mpbid 233 . . . . . . . 8 (((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) ∧ 𝑥𝑅𝑦) → ∃𝑢𝐴 𝑥𝑢)
3736ex 413 . . . . . . 7 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥𝑅𝑦 → ∃𝑢𝐴 𝑥𝑢))
3837pm4.71rd 563 . . . . . 6 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥𝑅𝑦 ↔ (∃𝑢𝐴 𝑥𝑢𝑥𝑅𝑦)))
39 r19.41v 3308 . . . . . 6 (∃𝑢𝐴 (𝑥𝑢𝑥𝑅𝑦) ↔ (∃𝑢𝐴 𝑥𝑢𝑥𝑅𝑦))
4038, 39syl6bbr 290 . . . . 5 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥𝑅𝑦 ↔ ∃𝑢𝐴 (𝑥𝑢𝑥𝑅𝑦)))
4121, 40bitr4d 283 . . . 4 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (∃𝑢𝐴 (𝑥𝑢𝑦𝑢) ↔ 𝑥𝑅𝑦))
426, 41syl5bb 284 . . 3 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → (𝑥𝐴𝑦𝑥𝑅𝑦))
432, 4, 42eqbrrdv 5552 . 2 ((𝑅𝑉 ∧ ( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴)) → ∼ 𝐴 = 𝑅)
4443ex 413 1 (𝑅𝑉 → (( EqvRel 𝑅 ∧ (dom 𝑅 / 𝑅) = 𝐴) → ∼ 𝐴 = 𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∃wrex 3106  Vcvv 3437  ∪ cuni 4745   class class class wbr 4962  dom cdm 5443  ran crn 5444  Rel wrel 5448  [cec 8137   / cqs 8138   ∼ ccoels 34986   EqvRel weqvrel 35002 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221  ax-un 7319 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-iun 4827  df-br 4963  df-opab 5025  df-id 5348  df-eprel 5353  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-ec 8141  df-qs 8145  df-coss 35190  df-coels 35191  df-refrel 35283  df-symrel 35311  df-trrel 35341  df-eqvrel 35351 This theorem is referenced by:  erim  35443
 Copyright terms: Public domain W3C validator