Description: Define the converse reflexive relation predicate (read: R is a converse reflexive relation), see also the comment of dfcnvrefrel3 . Alternate definitions are dfcnvrefrel2 and dfcnvrefrel3 . (Contributed by Peter Mazsa, 16-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-cnvrefrel | ⊢ ( CnvRefRel 𝑅 ↔ ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cR | ⊢ 𝑅 | |
| 1 | 0 | wcnvrefrel | ⊢ CnvRefRel 𝑅 |
| 2 | 0 | cdm | ⊢ dom 𝑅 |
| 3 | 0 | crn | ⊢ ran 𝑅 |
| 4 | 2 3 | cxp | ⊢ ( dom 𝑅 × ran 𝑅 ) |
| 5 | 0 4 | cin | ⊢ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) |
| 6 | cid | ⊢ I | |
| 7 | 6 4 | cin | ⊢ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) |
| 8 | 5 7 | wss | ⊢ ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) |
| 9 | 0 | wrel | ⊢ Rel 𝑅 |
| 10 | 8 9 | wa | ⊢ ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 ) |
| 11 | 1 10 | wb | ⊢ ( CnvRefRel 𝑅 ↔ ( ( 𝑅 ∩ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( I ∩ ( dom 𝑅 × ran 𝑅 ) ) ∧ Rel 𝑅 ) ) |