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 = dom dom G
Assertion ismgmOLD G A G Magma G : X × X X

Proof

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