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

Theorem iserd 7728
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 (𝜑 → Rel 𝑅)
iserd.2 ((𝜑𝑥𝑅𝑦) → 𝑦𝑅𝑥)
iserd.3 ((𝜑 ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧)
iserd.4 (𝜑 → (𝑥𝐴𝑥𝑅𝑥))
Assertion
Ref Expression
iserd (𝜑𝑅 Er 𝐴)
Distinct variable groups:   𝑥,𝑦,𝑧,𝑅   𝑥,𝐴   𝜑,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐴(𝑦,𝑧)

Proof of Theorem iserd
StepHypRef Expression
1 iserd.1 . . 3 (𝜑 → Rel 𝑅)
2 eqidd 2622 . . 3 (𝜑 → dom 𝑅 = dom 𝑅)
3 iserd.2 . . . . . . . 8 ((𝜑𝑥𝑅𝑦) → 𝑦𝑅𝑥)
43ex 450 . . . . . . 7 (𝜑 → (𝑥𝑅𝑦𝑦𝑅𝑥))
5 iserd.3 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧)
65ex 450 . . . . . . 7 (𝜑 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
74, 6jca 554 . . . . . 6 (𝜑 → ((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
87alrimiv 1852 . . . . 5 (𝜑 → ∀𝑧((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
98alrimiv 1852 . . . 4 (𝜑 → ∀𝑦𝑧((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
109alrimiv 1852 . . 3 (𝜑 → ∀𝑥𝑦𝑧((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
11 dfer2 7703 . . 3 (𝑅 Er dom 𝑅 ↔ (Rel 𝑅 ∧ dom 𝑅 = dom 𝑅 ∧ ∀𝑥𝑦𝑧((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
121, 2, 10, 11syl3anbrc 1244 . 2 (𝜑𝑅 Er dom 𝑅)
1312adantr 481 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝑅) → 𝑅 Er dom 𝑅)
14 simpr 477 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝑅) → 𝑥 ∈ dom 𝑅)
1513, 14erref 7722 . . . . . . 7 ((𝜑𝑥 ∈ dom 𝑅) → 𝑥𝑅𝑥)
1615ex 450 . . . . . 6 (𝜑 → (𝑥 ∈ dom 𝑅𝑥𝑅𝑥))
17 vex 3193 . . . . . . 7 𝑥 ∈ V
1817, 17breldm 5299 . . . . . 6 (𝑥𝑅𝑥𝑥 ∈ dom 𝑅)
1916, 18impbid1 215 . . . . 5 (𝜑 → (𝑥 ∈ dom 𝑅𝑥𝑅𝑥))
20 iserd.4 . . . . 5 (𝜑 → (𝑥𝐴𝑥𝑅𝑥))
2119, 20bitr4d 271 . . . 4 (𝜑 → (𝑥 ∈ dom 𝑅𝑥𝐴))
2221eqrdv 2619 . . 3 (𝜑 → dom 𝑅 = 𝐴)
23 ereq2 7710 . . 3 (dom 𝑅 = 𝐴 → (𝑅 Er dom 𝑅𝑅 Er 𝐴))
2422, 23syl 17 . 2 (𝜑 → (𝑅 Er dom 𝑅𝑅 Er 𝐴))
2512, 24mpbid 222 1 (𝜑𝑅 Er 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wcel 1987   class class class wbr 4623  dom cdm 5084  Rel wrel 5089   Er wer 7699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-er 7702
This theorem is referenced by:  iseri  7729  iseriALT  7730  swoer  7732  eqerOLD  7738  0erOLD  7741  iiner  7779  erinxp  7781  ecopoverOLD  7812  enerOLD  7963  cicer  16406  eqger  17584  gicerOLD  17659  gaorber  17681  efgrelexlemb  18103  efgcpbllemb  18108  hmpher  21527  xmeter  22178  phtpcerOLD  22735  vitalilem1OLD  23317  ercgrg  25346  metider  29761
  Copyright terms: Public domain W3C validator