Theorem clintopcllaw

Description: The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020)

	Ref	Expression
Assertion	clintopcllaw	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → ⚬ clLaw 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		clintop	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 )
2		ffnov	⊢ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ↔ ( ⚬ Fn ( 𝑀 × 𝑀 ) ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) )
3	2	simprbi	⊢ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 )
4	1 3	syl	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 )
5		elfvex	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → 𝑀 ∈ V )
6		iscllaw	⊢ ( ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ∧ 𝑀 ∈ V ) → ( ⚬ clLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) )
7	5 6	mpdan	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → ( ⚬ clLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ( 𝑥 ⚬ 𝑦 ) ∈ 𝑀 ) )
8	4 7	mpbird	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → ⚬ clLaw 𝑀 )