# 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 e. A -> ( G e. Magma <-> G : ( X X. X ) --> X ) )`

### Proof

Step Hyp Ref Expression
1 ismgmOLD.1
` |-  X = dom dom G`
2 feq1
` |-  ( g = G -> ( g : ( t X. t ) --> t <-> G : ( t X. t ) --> t ) )`
3 2 exbidv
` |-  ( g = G -> ( E. t g : ( t X. t ) --> t <-> E. t G : ( t X. t ) --> t ) )`
4 df-mgmOLD
` |-  Magma = { g | E. t g : ( t X. t ) --> t }`
5 3 4 elab2g
` |-  ( G e. A -> ( G e. Magma <-> E. t G : ( t X. t ) --> t ) )`
6 f00
` |-  ( G : ( (/) X. (/) ) --> (/) <-> ( G = (/) /\ ( (/) X. (/) ) = (/) ) )`
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 )`
` |-  ( ( G = (/) /\ ( (/) X. (/) ) = (/) ) -> (/) = dom dom G )`
15 6 14 sylbi
` |-  ( G : ( (/) X. (/) ) --> (/) -> (/) = dom dom G )`
16 xpeq12
` |-  ( ( t = (/) /\ t = (/) ) -> ( t X. t ) = ( (/) X. (/) ) )`
17 16 anidms
` |-  ( t = (/) -> ( t X. t ) = ( (/) X. (/) ) )`
18 feq23
` |-  ( ( ( t X. t ) = ( (/) X. (/) ) /\ t = (/) ) -> ( G : ( t X. t ) --> t <-> G : ( (/) X. (/) ) --> (/) ) )`
19 17 18 mpancom
` |-  ( t = (/) -> ( G : ( t X. t ) --> t <-> G : ( (/) X. (/) ) --> (/) ) )`
20 eqeq1
` |-  ( t = (/) -> ( t = dom dom G <-> (/) = dom dom G ) )`
21 19 20 imbi12d
` |-  ( t = (/) -> ( ( G : ( t X. t ) --> t -> t = dom dom G ) <-> ( G : ( (/) X. (/) ) --> (/) -> (/) = dom dom G ) ) )`
22 15 21 mpbiri
` |-  ( t = (/) -> ( G : ( t X. t ) --> t -> t = dom dom G ) )`
23 fdm
` |-  ( G : ( t X. t ) --> t -> dom G = ( t X. t ) )`
24 dmeq
` |-  ( dom G = ( t X. t ) -> dom dom G = dom ( t X. t ) )`
25 df-ne
` |-  ( t =/= (/) <-> -. t = (/) )`
26 dmxp
` |-  ( t =/= (/) -> dom ( t X. t ) = t )`
27 25 26 sylbir
` |-  ( -. t = (/) -> dom ( t X. t ) = t )`
28 27 eqeq1d
` |-  ( -. t = (/) -> ( dom ( t X. t ) = dom dom G <-> t = dom dom G ) )`
29 28 biimpcd
` |-  ( dom ( t X. t ) = dom dom G -> ( -. t = (/) -> t = dom dom G ) )`
30 29 eqcoms
` |-  ( dom dom G = dom ( t X. t ) -> ( -. t = (/) -> t = dom dom G ) )`
31 23 24 30 3syl
` |-  ( G : ( t X. t ) --> t -> ( -. t = (/) -> t = dom dom G ) )`
32 31 com12
` |-  ( -. t = (/) -> ( G : ( t X. t ) --> t -> t = dom dom G ) )`
33 22 32 pm2.61i
` |-  ( G : ( t X. t ) --> t -> t = dom dom G )`
34 33 pm4.71ri
` |-  ( G : ( t X. t ) --> t <-> ( t = dom dom G /\ G : ( t X. t ) --> t ) )`
35 34 exbii
` |-  ( E. t G : ( t X. t ) --> t <-> E. t ( t = dom dom G /\ G : ( t X. t ) --> t ) )`
36 5 35 syl6bb
` |-  ( G e. A -> ( G e. Magma <-> E. t ( t = dom dom G /\ G : ( t X. t ) --> t ) ) )`
37 dmexg
` |-  ( G e. A -> dom G e. _V )`
38 dmexg
` |-  ( dom G e. _V -> dom dom G e. _V )`
39 xpeq12
` |-  ( ( t = dom dom G /\ t = dom dom G ) -> ( t X. t ) = ( dom dom G X. dom dom G ) )`
40 39 anidms
` |-  ( t = dom dom G -> ( t X. t ) = ( dom dom G X. dom dom G ) )`
41 feq23
` |-  ( ( ( t X. t ) = ( dom dom G X. dom dom G ) /\ t = dom dom G ) -> ( G : ( t X. t ) --> t <-> G : ( dom dom G X. dom dom G ) --> dom dom G ) )`
42 40 41 mpancom
` |-  ( t = dom dom G -> ( G : ( t X. t ) --> t <-> G : ( dom dom G X. dom dom G ) --> dom dom G ) )`
43 1 eqcomi
` |-  dom dom G = X`
44 43 43 xpeq12i
` |-  ( dom dom G X. dom dom G ) = ( X X. X )`
45 44 43 feq23i
` |-  ( G : ( dom dom G X. dom dom G ) --> dom dom G <-> G : ( X X. X ) --> X )`
46 42 45 syl6bb
` |-  ( t = dom dom G -> ( G : ( t X. t ) --> t <-> G : ( X X. X ) --> X ) )`
47 46 ceqsexgv
` |-  ( dom dom G e. _V -> ( E. t ( t = dom dom G /\ G : ( t X. t ) --> t ) <-> G : ( X X. X ) --> X ) )`
48 37 38 47 3syl
` |-  ( G e. A -> ( E. t ( t = dom dom G /\ G : ( t X. t ) --> t ) <-> G : ( X X. X ) --> X ) )`
49 36 48 bitrd
` |-  ( G e. A -> ( G e. Magma <-> G : ( X X. X ) --> X ) )`