Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  refsymrel3 Structured version   Visualization version   GIF version

Theorem refsymrel3 36432
Description: A relation which is reflexive and symmetric (like an equivalence relation) can use the 𝑥 ∈ dom 𝑅𝑥𝑅𝑥 version for its reflexive part, not just the 𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) version of dfrefrel3 36384, cf. the comment of dfrefrel3 36384. (Contributed by Peter Mazsa, 23-Aug-2021.)
Assertion
Ref Expression
refsymrel3 (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ Rel 𝑅))
Distinct variable group:   𝑥,𝑅,𝑦

Proof of Theorem refsymrel3
StepHypRef Expression
1 dfrefrel3 36384 . . . 4 ( RefRel 𝑅 ↔ (∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ∧ Rel 𝑅))
2 dfsymrel3 36414 . . . 4 ( SymRel 𝑅 ↔ (∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥) ∧ Rel 𝑅))
31, 2anbi12i 630 . . 3 (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ∧ Rel 𝑅) ∧ (∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥) ∧ Rel 𝑅)))
4 anandi3r 1105 . . 3 ((∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ∧ Rel 𝑅 ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)) ↔ ((∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ∧ Rel 𝑅) ∧ (∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥) ∧ Rel 𝑅)))
5 3anan32 1099 . . 3 ((∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ∧ Rel 𝑅 ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)) ↔ ((∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ Rel 𝑅))
63, 4, 53bitr2i 302 . 2 (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ Rel 𝑅))
7 symrefref3 36428 . . . 4 (∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥) → (∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ↔ ∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥))
87pm5.32ri 579 . . 3 ((∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)) ↔ (∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)))
98anbi1i 627 . 2 (((∀𝑥 ∈ dom 𝑅𝑦 ∈ ran 𝑅(𝑥 = 𝑦𝑥𝑅𝑦) ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ Rel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ Rel 𝑅))
106, 9bitri 278 1 (( RefRel 𝑅 ∧ SymRel 𝑅) ↔ ((∀𝑥 ∈ dom 𝑅 𝑥𝑅𝑥 ∧ ∀𝑥𝑦(𝑥𝑅𝑦𝑦𝑅𝑥)) ∧ Rel 𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089  wal 1541  wral 3062   class class class wbr 5062  dom cdm 5560  ran crn 5561  Rel wrel 5565   RefRel wrefrel 36089   SymRel wsymrel 36095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5201  ax-nul 5208  ax-pr 5331
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3417  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-nul 4247  df-if 4449  df-sn 4551  df-pr 4553  df-op 4557  df-br 5063  df-opab 5125  df-id 5464  df-xp 5566  df-rel 5567  df-cnv 5568  df-dm 5570  df-rn 5571  df-res 5572  df-refrel 36380  df-symrel 36408
This theorem is referenced by:  dfeqvrel3  36454
  Copyright terms: Public domain W3C validator