Metamath Proof Explorer

Theorem isassintop

Description: The predicate "is an associative (closed internal binary) operations for a set". (Contributed by FL, 2-Nov-2009) (Revised by AV, 20-Jan-2020)

Ref Expression
Assertion isassintop ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ↔ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 assintopmap ⊢ ( 𝑀 ∈ 𝑉 → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } )
2 1 eleq2d ⊢ ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ↔ ⚬ ∈ { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } ) )
3 breq1 ⊢ ( 𝑜 = ⚬ → ( 𝑜 assLaw 𝑀 ↔ ⚬ assLaw 𝑀 ) )
4 3 elrab ⊢ ( ⚬ ∈ { 𝑜 ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∣ 𝑜 assLaw 𝑀 } ↔ ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ ⚬ assLaw 𝑀 ) )
5 2 4 bitrdi ⊢ ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ↔ ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ ⚬ assLaw 𝑀 ) ) )
6 elmapi ⊢ ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 )
7 6 ad2antrl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ ⚬ assLaw 𝑀 ) ) → ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 )
8 isasslaw ⊢ ( ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ 𝑀 ∈ 𝑉 ) → ( ⚬ assLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
9 8 biimpd ⊢ ( ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ 𝑀 ∈ 𝑉 ) → ( ⚬ assLaw 𝑀 → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
10 9 impancom ⊢ ( ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ ⚬ assLaw 𝑀 ) → ( 𝑀 ∈ 𝑉 → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
11 10 impcom ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ ⚬ assLaw 𝑀 ) ) → ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) )
12 7 11 jca ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ ⚬ assLaw 𝑀 ) ) → ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
13 12 ex ⊢ ( 𝑀 ∈ 𝑉 → ( ( ⚬ ∈ ( 𝑀 ↑m ( 𝑀 × 𝑀 ) ) ∧ ⚬ assLaw 𝑀 ) → ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) )
14 5 13 sylbid ⊢ ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) → ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) )
15 isclintop ⊢ ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ↔ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) )
16 15 biimprcd ⊢ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 → ( 𝑀 ∈ 𝑉 → ⚬ ∈ ( clIntOp ‘ 𝑀 ) ) )
17 16 adantr ⊢ ( ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) → ( 𝑀 ∈ 𝑉 → ⚬ ∈ ( clIntOp ‘ 𝑀 ) ) )
18 17 impcom ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) → ⚬ ∈ ( clIntOp ‘ 𝑀 ) )
19 sqxpexg ⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 × 𝑀 ) ∈ V )
20 fex ⊢ ( ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ( 𝑀 × 𝑀 ) ∈ V ) → ⚬ ∈ V )
21 19 20 sylan2 ⊢ ( ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ 𝑀 ∈ 𝑉 ) → ⚬ ∈ V )
22 21 ancoms ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) → ⚬ ∈ V )
23 simpl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) → 𝑀 ∈ 𝑉 )
24 isasslaw ⊢ ( ( ⚬ ∈ V ∧ 𝑀 ∈ 𝑉 ) → ( ⚬ assLaw 𝑀 ↔ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) )
25 24 bicomd ⊢ ( ( ⚬ ∈ V ∧ 𝑀 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ⚬ assLaw 𝑀 ) )
26 22 23 25 syl2anc ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) → ( ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ↔ ⚬ assLaw 𝑀 ) )
27 26 biimpd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ) → ( ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) → ⚬ assLaw 𝑀 ) )
28 27 impr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) → ⚬ assLaw 𝑀 )
29 assintopval ⊢ ( 𝑀 ∈ 𝑉 → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } )
30 29 adantr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) → ( assIntOp ‘ 𝑀 ) = { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } )
31 30 eleq2d ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ↔ ⚬ ∈ { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } ) )
32 3 elrab ⊢ ( ⚬ ∈ { 𝑜 ∈ ( clIntOp ‘ 𝑀 ) ∣ 𝑜 assLaw 𝑀 } ↔ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ∧ ⚬ assLaw 𝑀 ) )
33 31 32 bitrdi ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ↔ ( ⚬ ∈ ( clIntOp ‘ 𝑀 ) ∧ ⚬ assLaw 𝑀 ) ) )
34 18 28 33 mpbir2and ⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) → ⚬ ∈ ( assIntOp ‘ 𝑀 ) )
35 34 ex ⊢ ( 𝑀 ∈ 𝑉 → ( ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) → ⚬ ∈ ( assIntOp ‘ 𝑀 ) ) )
36 14 35 impbid ⊢ ( 𝑀 ∈ 𝑉 → ( ⚬ ∈ ( assIntOp ‘ 𝑀 ) ↔ ( ⚬ : ( 𝑀 × 𝑀 ) ⟶ 𝑀 ∧ ∀ 𝑥 ∈ 𝑀 ∀ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ( 𝑥 ⚬ 𝑦 ) ⚬ 𝑧 ) = ( 𝑥 ⚬ ( 𝑦 ⚬ 𝑧 ) ) ) ) )