Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  erth Structured version   Visualization version   GIF version

Theorem erth 8348
 Description: Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
Hypotheses
Ref Expression
erth.1 (𝜑𝑅 Er 𝑋)
erth.2 (𝜑𝐴𝑋)
Assertion
Ref Expression
erth (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))

Proof of Theorem erth
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 erth.1 . . . . . . . 8 (𝜑𝑅 Er 𝑋)
21ersymb 8313 . . . . . . 7 (𝜑 → (𝐴𝑅𝐵𝐵𝑅𝐴))
32biimpa 480 . . . . . 6 ((𝜑𝐴𝑅𝐵) → 𝐵𝑅𝐴)
41ertr 8314 . . . . . . 7 (𝜑 → ((𝐵𝑅𝐴𝐴𝑅𝑥) → 𝐵𝑅𝑥))
54impl 459 . . . . . 6 (((𝜑𝐵𝑅𝐴) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
63, 5syldanl 604 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
71ertr 8314 . . . . . 6 (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝑥) → 𝐴𝑅𝑥))
87impl 459 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥)
96, 8impbida 800 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝐴𝑅𝑥𝐵𝑅𝑥))
10 vex 3413 . . . . 5 𝑥 ∈ V
11 erth.2 . . . . . 6 (𝜑𝐴𝑋)
1211adantr 484 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐴𝑋)
13 elecg 8342 . . . . 5 ((𝑥 ∈ V ∧ 𝐴𝑋) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
1410, 12, 13sylancr 590 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
15 errel 8308 . . . . . . 7 (𝑅 Er 𝑋 → Rel 𝑅)
161, 15syl 17 . . . . . 6 (𝜑 → Rel 𝑅)
17 brrelex2 5575 . . . . . 6 ((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)
1816, 17sylan 583 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐵 ∈ V)
19 elecg 8342 . . . . 5 ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
2010, 18, 19sylancr 590 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
219, 14, 203bitr4d 314 . . 3 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝑥 ∈ [𝐵]𝑅))
2221eqrdv 2756 . 2 ((𝜑𝐴𝑅𝐵) → [𝐴]𝑅 = [𝐵]𝑅)
231adantr 484 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝑅 Er 𝑋)
241, 11erref 8319 . . . . . . 7 (𝜑𝐴𝑅𝐴)
2524adantr 484 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐴)
2611adantr 484 . . . . . . 7 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑋)
27 elecg 8342 . . . . . . 7 ((𝐴𝑋𝐴𝑋) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
2826, 26, 27syl2anc 587 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
2925, 28mpbird 260 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐴]𝑅)
30 simpr 488 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)
3129, 30eleqtrd 2854 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐵]𝑅)
3223, 30ereldm 8347 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴𝑋𝐵𝑋))
3326, 32mpbid 235 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑋)
34 elecg 8342 . . . . 5 ((𝐴𝑋𝐵𝑋) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3526, 33, 34syl2anc 587 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3631, 35mpbid 235 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑅𝐴)
3723, 36ersym 8311 . 2 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐵)
3822, 37impbida 800 1 (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3409   class class class wbr 5032  Rel wrel 5529   Er wer 8296  [cec 8297 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-br 5033  df-opab 5095  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-er 8299  df-ec 8301 This theorem is referenced by:  erth2  8349  erthi  8350  qliftfun  8392  eroveu  8402  eceqoveq  8412  enreceq  10526  prsrlem1  10532  ercpbllem  16879  orbsta  18510  sylow2blem3  18814  frgpnabllem2  19062  zndvds  20317  qustgpopn  22820  qustgphaus  22823  pi1xfrf  23754  pi1cof  23760  tgjustr  26367  qusvscpbl  31072  eqg0el  31078  nsgqusf1olem3  31121  pstmxmet  31368  sconnpi1  32717  topfneec2  34116
 Copyright terms: Public domain W3C validator