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

Theorem erth 8748
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 8713 . . . . . . 7 (𝜑 → (𝐴𝑅𝐵𝐵𝑅𝐴))
32biimpa 478 . . . . . 6 ((𝜑𝐴𝑅𝐵) → 𝐵𝑅𝐴)
41ertr 8714 . . . . . . 7 (𝜑 → ((𝐵𝑅𝐴𝐴𝑅𝑥) → 𝐵𝑅𝑥))
54impl 457 . . . . . 6 (((𝜑𝐵𝑅𝐴) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
63, 5syldanl 603 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
71ertr 8714 . . . . . 6 (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝑥) → 𝐴𝑅𝑥))
87impl 457 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥)
96, 8impbida 800 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝐴𝑅𝑥𝐵𝑅𝑥))
10 vex 3479 . . . . 5 𝑥 ∈ V
11 erth.2 . . . . . 6 (𝜑𝐴𝑋)
1211adantr 482 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐴𝑋)
13 elecg 8742 . . . . 5 ((𝑥 ∈ V ∧ 𝐴𝑋) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
1410, 12, 13sylancr 588 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
15 errel 8708 . . . . . . 7 (𝑅 Er 𝑋 → Rel 𝑅)
161, 15syl 17 . . . . . 6 (𝜑 → Rel 𝑅)
17 brrelex2 5728 . . . . . 6 ((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)
1816, 17sylan 581 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐵 ∈ V)
19 elecg 8742 . . . . 5 ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
2010, 18, 19sylancr 588 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
219, 14, 203bitr4d 311 . . 3 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝑥 ∈ [𝐵]𝑅))
2221eqrdv 2731 . 2 ((𝜑𝐴𝑅𝐵) → [𝐴]𝑅 = [𝐵]𝑅)
231adantr 482 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝑅 Er 𝑋)
241, 11erref 8719 . . . . . . 7 (𝜑𝐴𝑅𝐴)
2524adantr 482 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐴)
2611adantr 482 . . . . . . 7 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑋)
27 elecg 8742 . . . . . . 7 ((𝐴𝑋𝐴𝑋) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
2826, 26, 27syl2anc 585 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
2925, 28mpbird 257 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐴]𝑅)
30 simpr 486 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)
3129, 30eleqtrd 2836 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐵]𝑅)
3223, 30ereldm 8747 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴𝑋𝐵𝑋))
3326, 32mpbid 231 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑋)
34 elecg 8742 . . . . 5 ((𝐴𝑋𝐵𝑋) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3526, 33, 34syl2anc 585 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3631, 35mpbid 231 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑅𝐴)
3723, 36ersym 8711 . 2 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐵)
3822, 37impbida 800 1 (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  Vcvv 3475   class class class wbr 5147  Rel wrel 5680   Er wer 8696  [cec 8697
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-er 8699  df-ec 8701
This theorem is referenced by:  erth2  8749  erthi  8750  qliftfun  8792  eroveu  8802  eceqoveq  8812  enreceq  11057  prsrlem1  11063  ercpbllem  17490  orbsta  19171  sylow2blem3  19483  qusecsub  19695  frgpnabllem2  19734  zndvds  21089  qustgpopn  23606  qustgphaus  23609  pi1xfrf  24551  pi1cof  24557  tgjustr  27705  qusvscpbl  32435  eqg0el  32442  nsgqusf1olem3  32489  qsnzr  32532  pstmxmet  32815  sconnpi1  34168  topfneec2  35179
  Copyright terms: Public domain W3C validator