Step |
Hyp |
Ref |
Expression |
1 |
|
issmgrpOLD.1 |
⊢ 𝑋 = dom dom 𝐺 |
2 |
|
df-sgrOLD |
⊢ SemiGrp = ( Magma ∩ Ass ) |
3 |
2
|
eleq2i |
⊢ ( 𝐺 ∈ SemiGrp ↔ 𝐺 ∈ ( Magma ∩ Ass ) ) |
4 |
|
elin |
⊢ ( 𝐺 ∈ ( Magma ∩ Ass ) ↔ ( 𝐺 ∈ Magma ∧ 𝐺 ∈ Ass ) ) |
5 |
1
|
ismgmOLD |
⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ Magma ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ) |
6 |
1
|
isass |
⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ Ass ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) ) |
7 |
5 6
|
anbi12d |
⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝐺 ∈ Magma ∧ 𝐺 ∈ Ass ) ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) ) ) |
8 |
4 7
|
syl5bb |
⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ ( Magma ∩ Ass ) ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) ) ) |
9 |
3 8
|
syl5bb |
⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ SemiGrp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) ) ) |