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

Theorem erth 8796
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 8759 . . . . . . 7 (𝜑 → (𝐴𝑅𝐵𝐵𝑅𝐴))
32biimpa 476 . . . . . 6 ((𝜑𝐴𝑅𝐵) → 𝐵𝑅𝐴)
41ertr 8760 . . . . . . 7 (𝜑 → ((𝐵𝑅𝐴𝐴𝑅𝑥) → 𝐵𝑅𝑥))
54impl 455 . . . . . 6 (((𝜑𝐵𝑅𝐴) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
63, 5syldanl 602 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
71ertr 8760 . . . . . 6 (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝑥) → 𝐴𝑅𝑥))
87impl 455 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥)
96, 8impbida 801 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝐴𝑅𝑥𝐵𝑅𝑥))
10 vex 3484 . . . . 5 𝑥 ∈ V
11 erth.2 . . . . . 6 (𝜑𝐴𝑋)
1211adantr 480 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐴𝑋)
13 elecg 8789 . . . . 5 ((𝑥 ∈ V ∧ 𝐴𝑋) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
1410, 12, 13sylancr 587 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
15 errel 8754 . . . . . . 7 (𝑅 Er 𝑋 → Rel 𝑅)
161, 15syl 17 . . . . . 6 (𝜑 → Rel 𝑅)
17 brrelex2 5739 . . . . . 6 ((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)
1816, 17sylan 580 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐵 ∈ V)
19 elecg 8789 . . . . 5 ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
2010, 18, 19sylancr 587 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
219, 14, 203bitr4d 311 . . 3 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝑥 ∈ [𝐵]𝑅))
2221eqrdv 2735 . 2 ((𝜑𝐴𝑅𝐵) → [𝐴]𝑅 = [𝐵]𝑅)
231adantr 480 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝑅 Er 𝑋)
241, 11erref 8765 . . . . . . 7 (𝜑𝐴𝑅𝐴)
2524adantr 480 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐴)
2611adantr 480 . . . . . . 7 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑋)
27 elecg 8789 . . . . . . 7 ((𝐴𝑋𝐴𝑋) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
2826, 26, 27syl2anc 584 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
2925, 28mpbird 257 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐴]𝑅)
30 simpr 484 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)
3129, 30eleqtrd 2843 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐵]𝑅)
3223, 30ereldm 8795 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴𝑋𝐵𝑋))
3326, 32mpbid 232 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑋)
34 elecg 8789 . . . . 5 ((𝐴𝑋𝐵𝑋) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3526, 33, 34syl2anc 584 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3631, 35mpbid 232 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑅𝐴)
3723, 36ersym 8757 . 2 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐵)
3822, 37impbida 801 1 (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  Vcvv 3480   class class class wbr 5143  Rel wrel 5690   Er wer 8742  [cec 8743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-er 8745  df-ec 8747
This theorem is referenced by:  erth2  8797  erthi  8798  qliftfun  8842  eroveu  8852  eceqoveq  8862  enreceq  11106  prsrlem1  11112  ercpbllem  17593  eqg0el  19201  orbsta  19331  sylow2blem3  19640  qusecsub  19853  frgpnabllem2  19892  rngqipring1  21326  zndvds  21568  qustgpopn  24128  qustgphaus  24131  pi1xfrf  25086  pi1cof  25092  tgjustr  28482  rlocf1  33277  fracfld  33310  qusvscpbl  33379  nsgqusf1olem3  33443  qsnzr  33483  zringfrac  33582  pstmxmet  33896  sconnpi1  35244  topfneec2  36357
  Copyright terms: Public domain W3C validator