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

Theorem erth 7678
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 simpl 472 . . . . . . 7 ((𝜑𝐴𝑅𝐵) → 𝜑)
2 erth.1 . . . . . . . . 9 (𝜑𝑅 Er 𝑋)
32ersymb 7643 . . . . . . . 8 (𝜑 → (𝐴𝑅𝐵𝐵𝑅𝐴))
43biimpa 500 . . . . . . 7 ((𝜑𝐴𝑅𝐵) → 𝐵𝑅𝐴)
51, 4jca 553 . . . . . 6 ((𝜑𝐴𝑅𝐵) → (𝜑𝐵𝑅𝐴))
62ertr 7644 . . . . . . 7 (𝜑 → ((𝐵𝑅𝐴𝐴𝑅𝑥) → 𝐵𝑅𝑥))
76impl 648 . . . . . 6 (((𝜑𝐵𝑅𝐴) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
85, 7sylan 487 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
92ertr 7644 . . . . . 6 (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝑥) → 𝐴𝑅𝑥))
109impl 648 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥)
118, 10impbida 873 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝐴𝑅𝑥𝐵𝑅𝑥))
12 vex 3176 . . . . 5 𝑥 ∈ V
13 erth.2 . . . . . 6 (𝜑𝐴𝑋)
1413adantr 480 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐴𝑋)
15 elecg 7672 . . . . 5 ((𝑥 ∈ V ∧ 𝐴𝑋) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
1612, 14, 15sylancr 694 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
17 errel 7638 . . . . . . 7 (𝑅 Er 𝑋 → Rel 𝑅)
182, 17syl 17 . . . . . 6 (𝜑 → Rel 𝑅)
19 brrelex2 5081 . . . . . 6 ((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)
2018, 19sylan 487 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐵 ∈ V)
21 elecg 7672 . . . . 5 ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
2212, 20, 21sylancr 694 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
2311, 16, 223bitr4d 299 . . 3 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝑥 ∈ [𝐵]𝑅))
2423eqrdv 2608 . 2 ((𝜑𝐴𝑅𝐵) → [𝐴]𝑅 = [𝐵]𝑅)
252adantr 480 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝑅 Er 𝑋)
262, 13erref 7649 . . . . . . 7 (𝜑𝐴𝑅𝐴)
2726adantr 480 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐴)
2813adantr 480 . . . . . . 7 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑋)
29 elecg 7672 . . . . . . 7 ((𝐴𝑋𝐴𝑋) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
3028, 28, 29syl2anc 691 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
3127, 30mpbird 246 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐴]𝑅)
32 simpr 476 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)
3331, 32eleqtrd 2690 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐵]𝑅)
3425, 32ereldm 7677 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴𝑋𝐵𝑋))
3528, 34mpbid 221 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑋)
36 elecg 7672 . . . . 5 ((𝐴𝑋𝐵𝑋) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3728, 35, 36syl2anc 691 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3833, 37mpbid 221 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑅𝐴)
3925, 38ersym 7641 . 2 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐵)
4024, 39impbida 873 1 (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  Vcvv 3173   class class class wbr 4583  Rel wrel 5043   Er wer 7626  [cec 7627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-er 7629  df-ec 7631
This theorem is referenced by:  erth2  7679  erthi  7680  qliftfun  7719  eroveu  7729  eceqoveq  7740  enreceq  9766  prsrlem1  9772  ercpbllem  16031  orbsta  17569  sylow2blem3  17860  frgpnabllem2  18100  zndvds  19717  qustgpopn  21733  qustgphaus  21736  pi1xfrf  22661  pi1cof  22667  pstmxmet  29268  sconpi1  30475  topfneec2  31521
  Copyright terms: Public domain W3C validator