Theorem assintopass

Description: An associative (closed internal binary) operation for a set is associative. (Contributed by FL, 2-Nov-2009) (Revised by AV, 20-Jan-2020)

	Ref	Expression
Assertion	assintopass	⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ⚬ ∈ ( assIntOp ‘ 𝑀 ) )
2		elfvex	⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → 𝑀 ∈ V )
3		assintopasslaw	⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ⚬ assLaw 𝑀 )
4		isasslaw	⊢ ( ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ∧ 𝑀 ∈ V ) → ( ⚬ assLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
5	3 4	syl5ibcom	⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ( ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ∧ 𝑀 ∈ V ) → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
6	1 2 5	mp2and	⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )