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 \in A \to (G \in Magma \leftrightarrow G : X \times X ⟶ X)$

Proof

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

Metamath Proof Explorer

Theorem ismgmOLD

Proof