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

Theorem iserd 7148
Description: A reflexive, symmetric, transitive relation is an equivalence relation on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
Hypotheses
Ref Expression
iserd.1  |-  ( ph  ->  Rel  R )
iserd.2  |-  ( (
ph  /\  x R
y )  ->  y R x )
iserd.3  |-  ( (
ph  /\  ( x R y  /\  y R z ) )  ->  x R z )
iserd.4  |-  ( ph  ->  ( x  e.  A  <->  x R x ) )
Assertion
Ref Expression
iserd  |-  ( ph  ->  R  Er  A )
Distinct variable groups:    x, y,
z, R    x, A    ph, x, y, z
Allowed substitution hints:    A( y, z)

Proof of Theorem iserd
StepHypRef Expression
1 iserd.1 . . 3  |-  ( ph  ->  Rel  R )
2 eqidd 2444 . . 3  |-  ( ph  ->  dom  R  =  dom  R )
3 iserd.2 . . . . . . . 8  |-  ( (
ph  /\  x R
y )  ->  y R x )
43ex 434 . . . . . . 7  |-  ( ph  ->  ( x R y  ->  y R x ) )
5 iserd.3 . . . . . . . 8  |-  ( (
ph  /\  ( x R y  /\  y R z ) )  ->  x R z )
65ex 434 . . . . . . 7  |-  ( ph  ->  ( ( x R y  /\  y R z )  ->  x R z ) )
74, 6jca 532 . . . . . 6  |-  ( ph  ->  ( ( x R y  ->  y R x )  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) )
87alrimiv 1685 . . . . 5  |-  ( ph  ->  A. z ( ( x R y  -> 
y R x )  /\  ( ( x R y  /\  y R z )  ->  x R z ) ) )
98alrimiv 1685 . . . 4  |-  ( ph  ->  A. y A. z
( ( x R y  ->  y R x )  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) )
109alrimiv 1685 . . 3  |-  ( ph  ->  A. x A. y A. z ( ( x R y  ->  y R x )  /\  ( ( x R y  /\  y R z )  ->  x R z ) ) )
11 dfer2 7123 . . 3  |-  ( R  Er  dom  R  <->  ( Rel  R  /\  dom  R  =  dom  R  /\  A. x A. y A. z
( ( x R y  ->  y R x )  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) ) )
121, 2, 10, 11syl3anbrc 1172 . 2  |-  ( ph  ->  R  Er  dom  R
)
1312adantr 465 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  R )  ->  R  Er  dom  R )
14 simpr 461 . . . . . . . 8  |-  ( (
ph  /\  x  e.  dom  R )  ->  x  e.  dom  R )
1513, 14erref 7142 . . . . . . 7  |-  ( (
ph  /\  x  e.  dom  R )  ->  x R x )
1615ex 434 . . . . . 6  |-  ( ph  ->  ( x  e.  dom  R  ->  x R x ) )
17 vex 2996 . . . . . . 7  |-  x  e. 
_V
1817, 17breldm 5065 . . . . . 6  |-  ( x R x  ->  x  e.  dom  R )
1916, 18impbid1 203 . . . . 5  |-  ( ph  ->  ( x  e.  dom  R  <-> 
x R x ) )
20 iserd.4 . . . . 5  |-  ( ph  ->  ( x  e.  A  <->  x R x ) )
2119, 20bitr4d 256 . . . 4  |-  ( ph  ->  ( x  e.  dom  R  <-> 
x  e.  A ) )
2221eqrdv 2441 . . 3  |-  ( ph  ->  dom  R  =  A )
23 ereq2 7130 . . 3  |-  ( dom 
R  =  A  -> 
( R  Er  dom  R  <-> 
R  Er  A ) )
2422, 23syl 16 . 2  |-  ( ph  ->  ( R  Er  dom  R  <-> 
R  Er  A ) )
2512, 24mpbid 210 1  |-  ( ph  ->  R  Er  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1367    = wceq 1369    e. wcel 1756   class class class wbr 4313   dom cdm 4861   Rel wrel 4866    Er wer 7119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314  df-opab 4372  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-er 7122
This theorem is referenced by:  swoer  7150  eqer  7155  0er  7157  iiner  7193  erinxp  7195  ecopover  7225  ener  7377  eqger  15752  gicer  15825  gaorber  15847  efgrelexlemb  16268  efgcpbllemb  16273  hmpher  19379  xmeter  20030  phtpcer  20589  vitalilem1  21110  ercgrg  22991  metider  26343  erclwwlk  30512  erclwwlkn  30528
  Copyright terms: Public domain W3C validator