Description: Obsolete version of mgmcl as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | clmgmOLD.1 | ⊢ 𝑋 = dom dom 𝐺 | |
| Assertion | clmgmOLD | ⊢ ( ( 𝐺 ∈ Magma ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | clmgmOLD.1 | ⊢ 𝑋 = dom dom 𝐺 | |
| 2 | 1 | ismgmOLD | ⊢ ( 𝐺 ∈ Magma → ( 𝐺 ∈ Magma ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) ) |
| 3 | fovcdm | ⊢ ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) | |
| 4 | 3 | 3exp | ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) ) ) |
| 5 | 2 4 | biimtrdi | ⊢ ( 𝐺 ∈ Magma → ( 𝐺 ∈ Magma → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) ) ) ) |
| 6 | 5 | pm2.43i | ⊢ ( 𝐺 ∈ Magma → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) ) ) |
| 7 | 6 | 3imp | ⊢ ( ( 𝐺 ∈ Magma ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) |