Theorem iscllaw

Description: The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020)

	Ref	Expression
Assertion	iscllaw	⊢ ( ( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ) → ( ⚬ clLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
2		oveq	⊢ ( 𝑜 = ⚬ → ( 𝑥 𝑜 𝑦 ) = ( 𝑥 ⚬ 𝑦 ) )
3	2	adantr	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( 𝑥 𝑜 𝑦 ) = ( 𝑥 ⚬ 𝑦 ) )
4	3 1	eleq12d	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ( 𝑥 𝑜 𝑦 ) ∈ 𝑚 ↔ ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) )
5	1 4	raleqbidv	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) ∈ 𝑚 ↔ ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) )
6	1 5	raleqbidv	⊢ ( ( 𝑜 = ⚬ ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) ∈ 𝑚 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) )
7		df-cllaw	⊢ clLaw = { ⟨ 𝑜 , 𝑚 ⟩ ∣ ∀ 𝑥 ∈ 𝑚 ∀ 𝑦 ∈ 𝑚 ( 𝑥 𝑜 𝑦 ) ∈ 𝑚 }
8	6 7	brabga	⊢ ( ( ⚬ ∈ 𝑉 ∧ 𝑀 ∈ 𝑊 ) → ( ⚬ clLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) )