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

Metamath Proof Explorer

Theorem reldmevls1

Description: Well-behaved binary operation property of evalSub1 . (Contributed by AV, 7-Sep-2019)

Ref Expression
Assertion reldmevls1 ⊢ Rel ⁡ dom ⁡ evalSub 1

Proof

Step Hyp Ref Expression
1 df-evls1 ⊢ evalSub 1 = s ∈ V , r ∈ 𝒫 Base s ⟼ ⦋ Base s / b⦌ x ∈ b b 1 𝑜 ⟼ x ∘ y ∈ b ⟼ 1 𝑜 × y ∘ 1 𝑜 evalSub s ⁡ r
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ evalSub 1