Theorem reldmevls1

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

	Ref	Expression
Assertion	reldmevls1	⊢ Rel dom evalSub1

Proof

Step	Hyp	Ref	Expression
1		df-evls1	⊢ evalSub1 = ( 𝑠 ∈ V , 𝑟 ∈ 𝒫 ( Base ‘ 𝑠 ) ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( ( 𝑥 ∈ ( 𝑏 ↑m ( 𝑏 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( ( 1o evalSub 𝑠 ) ‘ 𝑟 ) ) )
2	1	reldmmpo	⊢ Rel dom evalSub1