Metamath Proof Explorer

Theorem assintop

Description: An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020)

Ref Expression
Assertion assintop ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ⚬ assLaw 𝑀 ) )

Proof

Step Hyp Ref Expression
1 elfvex ⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → 𝑀 ∈ V )
2 assintopmap ⊢ ( 𝑀 ∈ V → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } )
3 2 eleq2d ⊢ ( 𝑀 ∈ V → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ↔ ⚬ ∈ { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } ) )
4 breq1 ⊢ ( 𝑜 = ⚬ → ( 𝑜 assLaw 𝑀 ↔ ⚬ assLaw 𝑀 ) )
5 4 elrab ⊢ ( ⚬ ∈ { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } ↔ ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ ⚬ assLaw 𝑀 ) )
6 elmapi ⊢ ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 )
7 6 anim1i ⊢ ( ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ ⚬ assLaw 𝑀 ) → ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ⚬ assLaw 𝑀 ) )
8 5 7 sylbi ⊢ ( ⚬ ∈ { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } → ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ⚬ assLaw 𝑀 ) )
9 3 8 biimtrdi ⊢ ( 𝑀 ∈ V → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ⚬ assLaw 𝑀 ) ) )
10 1 9 mpcom ⊢ ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ⚬ assLaw 𝑀 ) )