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 ↾v

Proof

Step	Hyp	Ref	Expression
1		df-resv	⊢ ↾v = ( 𝑦 ∈ V , 𝑥 ∈ V ↦ if ( ( Base ‘ ( Scalar ‘ 𝑦 ) ) ⊆ 𝑥 , 𝑦 , ( 𝑦 sSet ⟨ ( Scalar ‘ ndx ) , ( ( Scalar ‘ 𝑦 ) ↾s 𝑥 ) ⟩ ) ) )
2	1	reldmmpo	⊢ Rel dom ↾v