# Metamath Proof Explorer

## Theorem ismgmOLD

Description: Obsolete version of ismgm as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis ismgmOLD.1 ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}$
Assertion ismgmOLD ${⊢}{G}\in {A}\to \left({G}\in \mathrm{Magma}↔{G}:{X}×{X}⟶{X}\right)$

### Proof

Step Hyp Ref Expression
1 ismgmOLD.1 ${⊢}{X}=\mathrm{dom}\mathrm{dom}{G}$
2 feq1 ${⊢}{g}={G}\to \left({g}:{t}×{t}⟶{t}↔{G}:{t}×{t}⟶{t}\right)$
3 2 exbidv ${⊢}{g}={G}\to \left(\exists {t}\phantom{\rule{.4em}{0ex}}{g}:{t}×{t}⟶{t}↔\exists {t}\phantom{\rule{.4em}{0ex}}{G}:{t}×{t}⟶{t}\right)$
4 df-mgmOLD ${⊢}\mathrm{Magma}=\left\{{g}|\exists {t}\phantom{\rule{.4em}{0ex}}{g}:{t}×{t}⟶{t}\right\}$
5 3 4 elab2g ${⊢}{G}\in {A}\to \left({G}\in \mathrm{Magma}↔\exists {t}\phantom{\rule{.4em}{0ex}}{G}:{t}×{t}⟶{t}\right)$
6 f00 ${⊢}{G}:\varnothing ×\varnothing ⟶\varnothing ↔\left({G}=\varnothing \wedge \varnothing ×\varnothing =\varnothing \right)$
7 dmeq ${⊢}{G}=\varnothing \to \mathrm{dom}{G}=\mathrm{dom}\varnothing$
8 dmeq ${⊢}\mathrm{dom}{G}=\mathrm{dom}\varnothing \to \mathrm{dom}\mathrm{dom}{G}=\mathrm{dom}\mathrm{dom}\varnothing$
9 dm0 ${⊢}\mathrm{dom}\varnothing =\varnothing$
10 9 dmeqi ${⊢}\mathrm{dom}\mathrm{dom}\varnothing =\mathrm{dom}\varnothing$
11 10 9 eqtri ${⊢}\mathrm{dom}\mathrm{dom}\varnothing =\varnothing$
12 8 11 syl6req ${⊢}\mathrm{dom}{G}=\mathrm{dom}\varnothing \to \varnothing =\mathrm{dom}\mathrm{dom}{G}$
13 7 12 syl ${⊢}{G}=\varnothing \to \varnothing =\mathrm{dom}\mathrm{dom}{G}$
14 13 adantr ${⊢}\left({G}=\varnothing \wedge \varnothing ×\varnothing =\varnothing \right)\to \varnothing =\mathrm{dom}\mathrm{dom}{G}$
15 6 14 sylbi ${⊢}{G}:\varnothing ×\varnothing ⟶\varnothing \to \varnothing =\mathrm{dom}\mathrm{dom}{G}$
16 xpeq12 ${⊢}\left({t}=\varnothing \wedge {t}=\varnothing \right)\to {t}×{t}=\varnothing ×\varnothing$
17 16 anidms ${⊢}{t}=\varnothing \to {t}×{t}=\varnothing ×\varnothing$
18 feq23 ${⊢}\left({t}×{t}=\varnothing ×\varnothing \wedge {t}=\varnothing \right)\to \left({G}:{t}×{t}⟶{t}↔{G}:\varnothing ×\varnothing ⟶\varnothing \right)$
19 17 18 mpancom ${⊢}{t}=\varnothing \to \left({G}:{t}×{t}⟶{t}↔{G}:\varnothing ×\varnothing ⟶\varnothing \right)$
20 eqeq1 ${⊢}{t}=\varnothing \to \left({t}=\mathrm{dom}\mathrm{dom}{G}↔\varnothing =\mathrm{dom}\mathrm{dom}{G}\right)$
21 19 20 imbi12d ${⊢}{t}=\varnothing \to \left(\left({G}:{t}×{t}⟶{t}\to {t}=\mathrm{dom}\mathrm{dom}{G}\right)↔\left({G}:\varnothing ×\varnothing ⟶\varnothing \to \varnothing =\mathrm{dom}\mathrm{dom}{G}\right)\right)$
22 15 21 mpbiri ${⊢}{t}=\varnothing \to \left({G}:{t}×{t}⟶{t}\to {t}=\mathrm{dom}\mathrm{dom}{G}\right)$
23 fdm ${⊢}{G}:{t}×{t}⟶{t}\to \mathrm{dom}{G}={t}×{t}$
24 dmeq ${⊢}\mathrm{dom}{G}={t}×{t}\to \mathrm{dom}\mathrm{dom}{G}=\mathrm{dom}\left({t}×{t}\right)$
25 df-ne ${⊢}{t}\ne \varnothing ↔¬{t}=\varnothing$
26 dmxp ${⊢}{t}\ne \varnothing \to \mathrm{dom}\left({t}×{t}\right)={t}$
27 25 26 sylbir ${⊢}¬{t}=\varnothing \to \mathrm{dom}\left({t}×{t}\right)={t}$
28 27 eqeq1d ${⊢}¬{t}=\varnothing \to \left(\mathrm{dom}\left({t}×{t}\right)=\mathrm{dom}\mathrm{dom}{G}↔{t}=\mathrm{dom}\mathrm{dom}{G}\right)$
29 28 biimpcd ${⊢}\mathrm{dom}\left({t}×{t}\right)=\mathrm{dom}\mathrm{dom}{G}\to \left(¬{t}=\varnothing \to {t}=\mathrm{dom}\mathrm{dom}{G}\right)$
30 29 eqcoms ${⊢}\mathrm{dom}\mathrm{dom}{G}=\mathrm{dom}\left({t}×{t}\right)\to \left(¬{t}=\varnothing \to {t}=\mathrm{dom}\mathrm{dom}{G}\right)$
31 23 24 30 3syl ${⊢}{G}:{t}×{t}⟶{t}\to \left(¬{t}=\varnothing \to {t}=\mathrm{dom}\mathrm{dom}{G}\right)$
32 31 com12 ${⊢}¬{t}=\varnothing \to \left({G}:{t}×{t}⟶{t}\to {t}=\mathrm{dom}\mathrm{dom}{G}\right)$
33 22 32 pm2.61i ${⊢}{G}:{t}×{t}⟶{t}\to {t}=\mathrm{dom}\mathrm{dom}{G}$
34 33 pm4.71ri ${⊢}{G}:{t}×{t}⟶{t}↔\left({t}=\mathrm{dom}\mathrm{dom}{G}\wedge {G}:{t}×{t}⟶{t}\right)$
35 34 exbii ${⊢}\exists {t}\phantom{\rule{.4em}{0ex}}{G}:{t}×{t}⟶{t}↔\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}=\mathrm{dom}\mathrm{dom}{G}\wedge {G}:{t}×{t}⟶{t}\right)$
36 5 35 syl6bb ${⊢}{G}\in {A}\to \left({G}\in \mathrm{Magma}↔\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}=\mathrm{dom}\mathrm{dom}{G}\wedge {G}:{t}×{t}⟶{t}\right)\right)$
37 dmexg ${⊢}{G}\in {A}\to \mathrm{dom}{G}\in \mathrm{V}$
38 dmexg ${⊢}\mathrm{dom}{G}\in \mathrm{V}\to \mathrm{dom}\mathrm{dom}{G}\in \mathrm{V}$
39 xpeq12 ${⊢}\left({t}=\mathrm{dom}\mathrm{dom}{G}\wedge {t}=\mathrm{dom}\mathrm{dom}{G}\right)\to {t}×{t}=\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}$
40 39 anidms ${⊢}{t}=\mathrm{dom}\mathrm{dom}{G}\to {t}×{t}=\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}$
41 feq23 ${⊢}\left({t}×{t}=\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}\wedge {t}=\mathrm{dom}\mathrm{dom}{G}\right)\to \left({G}:{t}×{t}⟶{t}↔{G}:\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}⟶\mathrm{dom}\mathrm{dom}{G}\right)$
42 40 41 mpancom ${⊢}{t}=\mathrm{dom}\mathrm{dom}{G}\to \left({G}:{t}×{t}⟶{t}↔{G}:\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}⟶\mathrm{dom}\mathrm{dom}{G}\right)$
43 1 eqcomi ${⊢}\mathrm{dom}\mathrm{dom}{G}={X}$
44 43 43 xpeq12i ${⊢}\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}={X}×{X}$
45 44 43 feq23i ${⊢}{G}:\mathrm{dom}\mathrm{dom}{G}×\mathrm{dom}\mathrm{dom}{G}⟶\mathrm{dom}\mathrm{dom}{G}↔{G}:{X}×{X}⟶{X}$
46 42 45 syl6bb ${⊢}{t}=\mathrm{dom}\mathrm{dom}{G}\to \left({G}:{t}×{t}⟶{t}↔{G}:{X}×{X}⟶{X}\right)$
47 46 ceqsexgv ${⊢}\mathrm{dom}\mathrm{dom}{G}\in \mathrm{V}\to \left(\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}=\mathrm{dom}\mathrm{dom}{G}\wedge {G}:{t}×{t}⟶{t}\right)↔{G}:{X}×{X}⟶{X}\right)$
48 37 38 47 3syl ${⊢}{G}\in {A}\to \left(\exists {t}\phantom{\rule{.4em}{0ex}}\left({t}=\mathrm{dom}\mathrm{dom}{G}\wedge {G}:{t}×{t}⟶{t}\right)↔{G}:{X}×{X}⟶{X}\right)$
49 36 48 bitrd ${⊢}{G}\in {A}\to \left({G}\in \mathrm{Magma}↔{G}:{X}×{X}⟶{X}\right)$