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

Theorem erth 7776
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 473 . . . . . . 7 ((𝜑𝐴𝑅𝐵) → 𝜑)
2 erth.1 . . . . . . . . 9 (𝜑𝑅 Er 𝑋)
32ersymb 7741 . . . . . . . 8 (𝜑 → (𝐴𝑅𝐵𝐵𝑅𝐴))
43biimpa 501 . . . . . . 7 ((𝜑𝐴𝑅𝐵) → 𝐵𝑅𝐴)
51, 4jca 554 . . . . . 6 ((𝜑𝐴𝑅𝐵) → (𝜑𝐵𝑅𝐴))
62ertr 7742 . . . . . . 7 (𝜑 → ((𝐵𝑅𝐴𝐴𝑅𝑥) → 𝐵𝑅𝑥))
76impl 649 . . . . . 6 (((𝜑𝐵𝑅𝐴) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
85, 7sylan 488 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐴𝑅𝑥) → 𝐵𝑅𝑥)
92ertr 7742 . . . . . 6 (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝑥) → 𝐴𝑅𝑥))
109impl 649 . . . . 5 (((𝜑𝐴𝑅𝐵) ∧ 𝐵𝑅𝑥) → 𝐴𝑅𝑥)
118, 10impbida 876 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝐴𝑅𝑥𝐵𝑅𝑥))
12 vex 3198 . . . . 5 𝑥 ∈ V
13 erth.2 . . . . . 6 (𝜑𝐴𝑋)
1413adantr 481 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐴𝑋)
15 elecg 7770 . . . . 5 ((𝑥 ∈ V ∧ 𝐴𝑋) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
1612, 14, 15sylancr 694 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝐴𝑅𝑥))
17 errel 7736 . . . . . . 7 (𝑅 Er 𝑋 → Rel 𝑅)
182, 17syl 17 . . . . . 6 (𝜑 → Rel 𝑅)
19 brrelex2 5147 . . . . . 6 ((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)
2018, 19sylan 488 . . . . 5 ((𝜑𝐴𝑅𝐵) → 𝐵 ∈ V)
21 elecg 7770 . . . . 5 ((𝑥 ∈ V ∧ 𝐵 ∈ V) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
2212, 20, 21sylancr 694 . . . 4 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐵]𝑅𝐵𝑅𝑥))
2311, 16, 223bitr4d 300 . . 3 ((𝜑𝐴𝑅𝐵) → (𝑥 ∈ [𝐴]𝑅𝑥 ∈ [𝐵]𝑅))
2423eqrdv 2618 . 2 ((𝜑𝐴𝑅𝐵) → [𝐴]𝑅 = [𝐵]𝑅)
252adantr 481 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝑅 Er 𝑋)
262, 13erref 7747 . . . . . . 7 (𝜑𝐴𝑅𝐴)
2726adantr 481 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐴)
2813adantr 481 . . . . . . 7 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑋)
29 elecg 7770 . . . . . . 7 ((𝐴𝑋𝐴𝑋) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
3028, 28, 29syl2anc 692 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐴]𝑅𝐴𝑅𝐴))
3127, 30mpbird 247 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐴]𝑅)
32 simpr 477 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → [𝐴]𝑅 = [𝐵]𝑅)
3331, 32eleqtrd 2701 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴 ∈ [𝐵]𝑅)
3425, 32ereldm 7775 . . . . . 6 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴𝑋𝐵𝑋))
3528, 34mpbid 222 . . . . 5 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑋)
36 elecg 7770 . . . . 5 ((𝐴𝑋𝐵𝑋) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3728, 35, 36syl2anc 692 . . . 4 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → (𝐴 ∈ [𝐵]𝑅𝐵𝑅𝐴))
3833, 37mpbid 222 . . 3 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐵𝑅𝐴)
3925, 38ersym 7739 . 2 ((𝜑 ∧ [𝐴]𝑅 = [𝐵]𝑅) → 𝐴𝑅𝐵)
4024, 39impbida 876 1 (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  Vcvv 3195   class class class wbr 4644  Rel wrel 5109   Er wer 7724  [cec 7725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-er 7727  df-ec 7729
This theorem is referenced by:  erth2  7777  erthi  7778  qliftfun  7817  eroveu  7827  eceqoveq  7838  enreceq  9872  prsrlem1  9878  ercpbllem  16189  orbsta  17727  sylow2blem3  18018  frgpnabllem2  18258  zndvds  19879  qustgpopn  21904  qustgphaus  21907  pi1xfrf  22834  pi1cof  22840  pstmxmet  29914  sconnpi1  31195  topfneec2  32326
  Copyright terms: Public domain W3C validator