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

Theorem erth 6590
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  |-  ( ph  ->  R  Er  X )
erth.2  |-  ( ph  ->  A  e.  X )
Assertion
Ref Expression
erth  |-  ( ph  ->  ( A R B  <->  [ A ] R  =  [ B ] R
) )

Proof of Theorem erth
StepHypRef Expression
1 simpl 445 . . . . . . 7  |-  ( (
ph  /\  A R B )  ->  ph )
2 erth.1 . . . . . . . . 9  |-  ( ph  ->  R  Er  X )
32ersymb 6560 . . . . . . . 8  |-  ( ph  ->  ( A R B  <-> 
B R A ) )
43biimpa 472 . . . . . . 7  |-  ( (
ph  /\  A R B )  ->  B R A )
51, 4jca 520 . . . . . 6  |-  ( (
ph  /\  A R B )  ->  ( ph  /\  B R A ) )
62ertr 6561 . . . . . . 7  |-  ( ph  ->  ( ( B R A  /\  A R x )  ->  B R x ) )
76impl 606 . . . . . 6  |-  ( ( ( ph  /\  B R A )  /\  A R x )  ->  B R x )
85, 7sylan 459 . . . . 5  |-  ( ( ( ph  /\  A R B )  /\  A R x )  ->  B R x )
92ertr 6561 . . . . . 6  |-  ( ph  ->  ( ( A R B  /\  B R x )  ->  A R x ) )
109impl 606 . . . . 5  |-  ( ( ( ph  /\  A R B )  /\  B R x )  ->  A R x )
118, 10impbida 808 . . . 4  |-  ( (
ph  /\  A R B )  ->  ( A R x  <->  B R x ) )
12 vex 2730 . . . . 5  |-  x  e. 
_V
13 erth.2 . . . . . 6  |-  ( ph  ->  A  e.  X )
1413adantr 453 . . . . 5  |-  ( (
ph  /\  A R B )  ->  A  e.  X )
15 elecg 6584 . . . . 5  |-  ( ( x  e.  _V  /\  A  e.  X )  ->  ( x  e.  [ A ] R  <->  A R x ) )
1612, 14, 15sylancr 647 . . . 4  |-  ( (
ph  /\  A R B )  ->  (
x  e.  [ A ] R  <->  A R x ) )
17 errel 6555 . . . . . . 7  |-  ( R  Er  X  ->  Rel  R )
182, 17syl 17 . . . . . 6  |-  ( ph  ->  Rel  R )
19 brrelex2 4635 . . . . . 6  |-  ( ( Rel  R  /\  A R B )  ->  B  e.  _V )
2018, 19sylan 459 . . . . 5  |-  ( (
ph  /\  A R B )  ->  B  e.  _V )
21 elecg 6584 . . . . 5  |-  ( ( x  e.  _V  /\  B  e.  _V )  ->  ( x  e.  [ B ] R  <->  B R x ) )
2212, 20, 21sylancr 647 . . . 4  |-  ( (
ph  /\  A R B )  ->  (
x  e.  [ B ] R  <->  B R x ) )
2311, 16, 223bitr4d 278 . . 3  |-  ( (
ph  /\  A R B )  ->  (
x  e.  [ A ] R  <->  x  e.  [ B ] R ) )
2423eqrdv 2251 . 2  |-  ( (
ph  /\  A R B )  ->  [ A ] R  =  [ B ] R )
252adantr 453 . . 3  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  R  Er  X )
262, 13erref 6566 . . . . . . 7  |-  ( ph  ->  A R A )
2726adantr 453 . . . . . 6  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A R A )
2813adantr 453 . . . . . . 7  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A  e.  X )
29 elecg 6584 . . . . . . 7  |-  ( ( A  e.  X  /\  A  e.  X )  ->  ( A  e.  [ A ] R  <->  A R A ) )
3028, 28, 29syl2anc 645 . . . . . 6  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  -> 
( A  e.  [ A ] R  <->  A R A ) )
3127, 30mpbird 225 . . . . 5  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A  e.  [ A ] R )
32 simpr 449 . . . . 5  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  [ A ] R  =  [ B ] R
)
3331, 32eleqtrd 2329 . . . 4  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A  e.  [ B ] R )
3425, 32ereldm 6589 . . . . . 6  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  -> 
( A  e.  X  <->  B  e.  X ) )
3528, 34mpbid 203 . . . . 5  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  B  e.  X )
36 elecg 6584 . . . . 5  |-  ( ( A  e.  X  /\  B  e.  X )  ->  ( A  e.  [ B ] R  <->  B R A ) )
3728, 35, 36syl2anc 645 . . . 4  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  -> 
( A  e.  [ B ] R  <->  B R A ) )
3833, 37mpbid 203 . . 3  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  B R A )
3925, 38ersym 6558 . 2  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A R B )
4024, 39impbida 808 1  |-  ( ph  ->  ( A R B  <->  [ A ] R  =  [ B ] R
) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    = wceq 1619    e. wcel 1621   _Vcvv 2727   class class class wbr 3920   Rel wrel 4585    Er wer 6543   [cec 6544
This theorem is referenced by:  erth2  6591  erthi  6592  qliftfun  6629  eroveu  6639  eceqoveq  6649  th3qlem1  6650  enreceq  8571  ercpbllem  13324  orbsta  14602  sylow2blem3  14768  frgpnabllem2  14997  zndvds  16335  divstgpopn  17634  divstgphaus  17637  pi1xfrf  18383  pi1cof  18389  sconpi1  22941  topfneec2  25458
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-br 3921  df-opab 3975  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-er 6546  df-ec 6548
  Copyright terms: Public domain W3C validator