| Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-cnvrefrel | Structured version Visualization version GIF version | ||
| Description: Define the converse reflexive relation predicate (read: 𝑅 is a converse reflexive relation), see also the comment of dfcnvrefrel3 38532. Alternate definitions are dfcnvrefrel2 38531 and dfcnvrefrel3 38532. (Contributed by Peter Mazsa, 16-Jul-2021.) |
| Ref | Expression |
|---|---|
| df-cnvrefrel | ⊢ ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cR | . . 3 class 𝑅 | |
| 2 | 1 | wcnvrefrel 38191 | . 2 wff CnvRefRel 𝑅 |
| 3 | 1 | cdm 5685 | . . . . . 6 class dom 𝑅 |
| 4 | 1 | crn 5686 | . . . . . 6 class ran 𝑅 |
| 5 | 3, 4 | cxp 5683 | . . . . 5 class (dom 𝑅 × ran 𝑅) |
| 6 | 1, 5 | cin 3950 | . . . 4 class (𝑅 ∩ (dom 𝑅 × ran 𝑅)) |
| 7 | cid 5577 | . . . . 5 class I | |
| 8 | 7, 5 | cin 3950 | . . . 4 class ( I ∩ (dom 𝑅 × ran 𝑅)) |
| 9 | 6, 8 | wss 3951 | . . 3 wff (𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) |
| 10 | 1 | wrel 5690 | . . 3 wff Rel 𝑅 |
| 11 | 9, 10 | wa 395 | . 2 wff ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅) |
| 12 | 2, 11 | wb 206 | 1 wff ( CnvRefRel 𝑅 ↔ ((𝑅 ∩ (dom 𝑅 × ran 𝑅)) ⊆ ( I ∩ (dom 𝑅 × ran 𝑅)) ∧ Rel 𝑅)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfcnvrefrel2 38531 dfcnvrefrel3 38532 dfcnvrefrel4 38533 |
| Copyright terms: Public domain | W3C validator |