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

Metamath Proof Explorer

Theorem ismgmOLD

Proof