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

Definition df-cnvrefrel 38508
Description: Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 38512. Alternate definitions are dfcnvrefrel2 38511 and dfcnvrefrel3 38512. (Contributed by Peter Mazsa, 16-Jul-2021.)
Assertion
Ref Expression
df-cnvrefrel ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))

Detailed syntax breakdown of Definition df-cnvrefrel
StepHypRef Expression
1 cR . . 3 class 𝑅
21wcnvrefrel 38170 . 2 wff CnvRefRel 𝑅
31cdm 5688 . . . . . 6 class dom 𝑅
41crn 5689 . . . . . 6 class ran 𝑅
53, 4cxp 5686 . . . . 5 class (dom 𝑅 × ran 𝑅)
61, 5cin 3961 . . . 4 class (𝑅 ∩ (dom 𝑅 × ran 𝑅))
7 cid 5581 . . . . 5 class I
87, 5cin 3961 . . . 4 class ( I ∩ (dom 𝑅 × ran 𝑅))
96, 8wss 3962 . . 3 wff (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅))
101wrel 5693 . . 3 wff Rel 𝑅
119, 10wa 395 . 2 wff ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)
122, 11wb 206 1 wff ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅))
Colors of variables: wff setvar class
This definition is referenced by:  dfcnvrefrel2  38511  dfcnvrefrel3  38512  dfcnvrefrel4  38513
  Copyright terms: Public domain W3C validator