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 ) )