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

Metamath Proof Explorer

Theorem reldmresv

Description: The scalar restriction is a proper operator, so it can be used with ovprc1 . (Contributed by Thierry Arnoux, 6-Sep-2018)

Ref Expression
Assertion reldmresv ⊢ Rel ⁡ dom ⁡ ↾ 𝑣

Proof

Step Hyp Ref Expression
1 df-resv ⊢ ↾ 𝑣 = y ∈ V , x ∈ V ⟼ if Base Scalar ⁡ y ⊆ x y y sSet Scalar ⁡ ndx Scalar ⁡ y ↾ 𝑠 x
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ ↾ 𝑣