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

Theorem iserd 7655
 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 2611 . . 3 (𝜑 → dom 𝑅 = dom 𝑅)
3 iserd.2 . . . . . . . 8 ((𝜑𝑥𝑅𝑦) → 𝑦𝑅𝑥)
43ex 449 . . . . . . 7 (𝜑 → (𝑥𝑅𝑦𝑦𝑅𝑥))
5 iserd.3 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑅𝑦𝑦𝑅𝑧)) → 𝑥𝑅𝑧)
65ex 449 . . . . . . 7 (𝜑 → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))
74, 6jca 553 . . . . . 6 (𝜑 → ((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
87alrimiv 1842 . . . . 5 (𝜑 → ∀𝑧((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
98alrimiv 1842 . . . 4 (𝜑 → ∀𝑦𝑧((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
109alrimiv 1842 . . 3 (𝜑 → ∀𝑥𝑦𝑧((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
11 dfer2 7630 . . 3 (𝑅 Er dom 𝑅 ↔ (Rel 𝑅 ∧ dom 𝑅 = dom 𝑅 ∧ ∀𝑥𝑦𝑧((𝑥𝑅𝑦𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))))
121, 2, 10, 11syl3anbrc 1239 . 2 (𝜑𝑅 Er dom 𝑅)
1312adantr 480 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝑅) → 𝑅 Er dom 𝑅)
14 simpr 476 . . . . . . . 8 ((𝜑𝑥 ∈ dom 𝑅) → 𝑥 ∈ dom 𝑅)
1513, 14erref 7649 . . . . . . 7 ((𝜑𝑥 ∈ dom 𝑅) → 𝑥𝑅𝑥)
1615ex 449 . . . . . 6 (𝜑 → (𝑥 ∈ dom 𝑅𝑥𝑅𝑥))
17 vex 3176 . . . . . . 7 𝑥 ∈ V
1817, 17breldm 5251 . . . . . 6 (𝑥𝑅𝑥𝑥 ∈ dom 𝑅)
1916, 18impbid1 214 . . . . 5 (𝜑 → (𝑥 ∈ dom 𝑅𝑥𝑅𝑥))
20 iserd.4 . . . . 5 (𝜑 → (𝑥𝐴𝑥𝑅𝑥))
2119, 20bitr4d 270 . . . 4 (𝜑 → (𝑥 ∈ dom 𝑅𝑥𝐴))
2221eqrdv 2608 . . 3 (𝜑 → dom 𝑅 = 𝐴)
23 ereq2 7637 . . 3 (dom 𝑅 = 𝐴 → (𝑅 Er dom 𝑅𝑅 Er 𝐴))
2422, 23syl 17 . 2 (𝜑 → (𝑅 Er dom 𝑅𝑅 Er 𝐴))
2512, 24mpbid 221 1 (𝜑𝑅 Er 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  dom cdm 5038  Rel wrel 5043   Er wer 7626 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-er 7629 This theorem is referenced by:  iseri  7656  iseriALT  7657  swoer  7659  eqerOLD  7665  0erOLD  7668  iiner  7706  erinxp  7708  ecopoverOLD  7739  enerOLD  7889  cicer  16289  eqger  17467  gicerOLD  17542  gaorber  17564  efgrelexlemb  17986  efgcpbllemb  17991  hmpher  21397  xmeter  22048  phtpcerOLD  22603  vitalilem1OLD  23183  ercgrg  25212  metider  29265
 Copyright terms: Public domain W3C validator