This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnqmap

Description: The range of the quotient map is the quotient carrier. It lets us replace quotient-carrier reasoning by map/range reasoning (and conversely) via df-qmap and dfqs2 . (Contributed by Peter Mazsa, 12-Feb-2026)

Ref Expression
Assertion rnqmap Could not format assertion : No typesetting found for |- ran QMap R = ( dom R /. R ) with typecode |-

Proof

Step Hyp Ref Expression
1 df-qmap Could not format QMap R = ( x e. dom R |-> [ x ] R ) : No typesetting found for |- QMap R = ( x e. dom R |-> [ x ] R ) with typecode |-
2 1 rneqi Could not format ran QMap R = ran ( x e. dom R |-> [ x ] R ) : No typesetting found for |- ran QMap R = ran ( x e. dom R |-> [ x ] R ) with typecode |-
3 dfqs2 ⊢ dom ⁡ R / R = ran ⁡ x ∈ dom ⁡ R ⟼ x R
4 2 3 eqtr4i Could not format ran QMap R = ( dom R /. R ) : No typesetting found for |- ran QMap R = ( dom R /. R ) with typecode |-