This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Symmetric relation implies that the domain and the range are equal.
(Contributed by Peter Mazsa, 29-Dec-2021)
|
|
Ref |
Expression |
|
Assertion |
symrelim |
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅 ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
rncnv |
⊢ ran ◡ 𝑅 = dom 𝑅 |
| 2 |
|
dfsymrel4 |
⊢ ( SymRel 𝑅 ↔ ( ◡ 𝑅 = 𝑅 ∧ Rel 𝑅 ) ) |
| 3 |
2
|
simplbi |
⊢ ( SymRel 𝑅 → ◡ 𝑅 = 𝑅 ) |
| 4 |
3
|
rneqd |
⊢ ( SymRel 𝑅 → ran ◡ 𝑅 = ran 𝑅 ) |
| 5 |
1 4
|
eqtr3id |
⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅 ) |