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 )
14 13 adantr
 |-  ( ( 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 bitrdi
 |-  ( 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 bitrdi
 |-  ( 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 ) )