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

Theorem erth 6912
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 simpl 444 . . . . . . 7  |-  ( (
ph  /\  A R B )  ->  ph )
2 erth.1 . . . . . . . . 9  |-  ( ph  ->  R  Er  X )
32ersymb 6882 . . . . . . . 8  |-  ( ph  ->  ( A R B  <-> 
B R A ) )
43biimpa 471 . . . . . . 7  |-  ( (
ph  /\  A R B )  ->  B R A )
51, 4jca 519 . . . . . 6  |-  ( (
ph  /\  A R B )  ->  ( ph  /\  B R A ) )
62ertr 6883 . . . . . . 7  |-  ( ph  ->  ( ( B R A  /\  A R x )  ->  B R x ) )
76impl 604 . . . . . 6  |-  ( ( ( ph  /\  B R A )  /\  A R x )  ->  B R x )
85, 7sylan 458 . . . . 5  |-  ( ( ( ph  /\  A R B )  /\  A R x )  ->  B R x )
92ertr 6883 . . . . . 6  |-  ( ph  ->  ( ( A R B  /\  B R x )  ->  A R x ) )
109impl 604 . . . . 5  |-  ( ( ( ph  /\  A R B )  /\  B R x )  ->  A R x )
118, 10impbida 806 . . . 4  |-  ( (
ph  /\  A R B )  ->  ( A R x  <->  B R x ) )
12 vex 2923 . . . . 5  |-  x  e. 
_V
13 erth.2 . . . . . 6  |-  ( ph  ->  A  e.  X )
1413adantr 452 . . . . 5  |-  ( (
ph  /\  A R B )  ->  A  e.  X )
15 elecg 6906 . . . . 5  |-  ( ( x  e.  _V  /\  A  e.  X )  ->  ( x  e.  [ A ] R  <->  A R x ) )
1612, 14, 15sylancr 645 . . . 4  |-  ( (
ph  /\  A R B )  ->  (
x  e.  [ A ] R  <->  A R x ) )
17 errel 6877 . . . . . . 7  |-  ( R  Er  X  ->  Rel  R )
182, 17syl 16 . . . . . 6  |-  ( ph  ->  Rel  R )
19 brrelex2 4880 . . . . . 6  |-  ( ( Rel  R  /\  A R B )  ->  B  e.  _V )
2018, 19sylan 458 . . . . 5  |-  ( (
ph  /\  A R B )  ->  B  e.  _V )
21 elecg 6906 . . . . 5  |-  ( ( x  e.  _V  /\  B  e.  _V )  ->  ( x  e.  [ B ] R  <->  B R x ) )
2212, 20, 21sylancr 645 . . . 4  |-  ( (
ph  /\  A R B )  ->  (
x  e.  [ B ] R  <->  B R x ) )
2311, 16, 223bitr4d 277 . . 3  |-  ( (
ph  /\  A R B )  ->  (
x  e.  [ A ] R  <->  x  e.  [ B ] R ) )
2423eqrdv 2406 . 2  |-  ( (
ph  /\  A R B )  ->  [ A ] R  =  [ B ] R )
252adantr 452 . . 3  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  R  Er  X )
262, 13erref 6888 . . . . . . 7  |-  ( ph  ->  A R A )
2726adantr 452 . . . . . 6  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A R A )
2813adantr 452 . . . . . . 7  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A  e.  X )
29 elecg 6906 . . . . . . 7  |-  ( ( A  e.  X  /\  A  e.  X )  ->  ( A  e.  [ A ] R  <->  A R A ) )
3028, 28, 29syl2anc 643 . . . . . 6  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  -> 
( A  e.  [ A ] R  <->  A R A ) )
3127, 30mpbird 224 . . . . 5  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A  e.  [ A ] R )
32 simpr 448 . . . . 5  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  [ A ] R  =  [ B ] R
)
3331, 32eleqtrd 2484 . . . 4  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A  e.  [ B ] R )
3425, 32ereldm 6911 . . . . . 6  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  -> 
( A  e.  X  <->  B  e.  X ) )
3528, 34mpbid 202 . . . . 5  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  B  e.  X )
36 elecg 6906 . . . . 5  |-  ( ( A  e.  X  /\  B  e.  X )  ->  ( A  e.  [ B ] R  <->  B R A ) )
3728, 35, 36syl2anc 643 . . . 4  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  -> 
( A  e.  [ B ] R  <->  B R A ) )
3833, 37mpbid 202 . . 3  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  B R A )
3925, 38ersym 6880 . 2  |-  ( (
ph  /\  [ A ] R  =  [ B ] R )  ->  A R B )
4024, 39impbida 806 1  |-  ( ph  ->  ( A R B  <->  [ A ] R  =  [ B ] R
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721   _Vcvv 2920   class class class wbr 4176   Rel wrel 4846    Er wer 6865   [cec 6866
This theorem is referenced by:  erth2  6913  erthi  6914  qliftfun  6952  eroveu  6962  eceqoveq  6972  th3qlem1  6973  enreceq  8904  ercpbllem  13732  orbsta  15049  sylow2blem3  15215  frgpnabllem2  15444  zndvds  16789  divstgpopn  18106  divstgphaus  18109  pi1xfrf  19035  pi1cof  19041  pstmxmet  24249  sconpi1  24883  topfneec2  26266
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177  df-opab 4231  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-er 6868  df-ec 6870
  Copyright terms: Public domain W3C validator