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

Definition df-symrel 34784
Description: Define the symmetric relation predicate. (Read: 𝑅 is a symmetric relation.) For sets, being an element of the class of symmetric relations (df-symrels 34783) is equivalent to satisfying the symmetric relation predicate, cf. elsymrelsrel 34797. Alternate definitions are dfsymrel2 34789 and dfsymrel3 34790. (Contributed by Peter Mazsa, 16-Jul-2021.)
Assertion
Ref Expression
df-symrel ( SymRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))

Detailed syntax breakdown of Definition df-symrel
StepHypRef Expression
1 cR . . 3 class 𝑅
21wsymrel 34481 . 2 wff SymRel 𝑅
31cdm 5312 . . . . . . 7 class dom 𝑅
41crn 5313 . . . . . . 7 class ran 𝑅
53, 4cxp 5310 . . . . . 6 class (dom 𝑅 × ran 𝑅)
61, 5cin 3768 . . . . 5 class (𝑅 ∩ (dom 𝑅 × ran 𝑅))
76ccnv 5311 . . . 4 class (𝑅 ∩ (dom 𝑅 × ran 𝑅))
87, 6wss 3769 . . 3 wff (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅))
91wrel 5317 . . 3 wff Rel 𝑅
108, 9wa 385 . 2 wff ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)
112, 10wb 198 1 wff ( SymRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Colors of variables: wff setvar class
This definition is referenced by:  dfsymrel2  34789
  Copyright terms: Public domain W3C validator