Theorem assintopcllaw

Description: The closure low holds for an associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009) (Revised by AV, 20-Jan-2020)

	Ref	Expression
Assertion	assintopcllaw	⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ⚬ clLaw 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		elfvex	⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → 𝑀 ∈ V )
2		assintopval	⊢ ( 𝑀 ∈ V → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } )
3	2	eleq2d	⊢ ( 𝑀 ∈ V → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ↔ ⚬ ∈ { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } ) )
4		breq1	⊢ ( 𝑜 = ⚬ → ( 𝑜 assLaw 𝑀 ↔ ⚬ assLaw 𝑀 ) )
5	4	elrab	⊢ ( ⚬ ∈ { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } ↔ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ∧ ⚬ assLaw 𝑀 ) )
6	3 5	bitrdi	⊢ ( 𝑀 ∈ V → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ↔ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ∧ ⚬ assLaw 𝑀 ) ) )
7		clintopcllaw	⊢ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) → ⚬ clLaw 𝑀 )
8	7	adantr	⊢ ( ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ∧ ⚬ assLaw 𝑀 ) → ⚬ clLaw 𝑀 )
9	6 8	biimtrdi	⊢ ( 𝑀 ∈ V → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ⚬ clLaw 𝑀 ) )
10	1 9	mpcom	⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ⚬ clLaw 𝑀 )