degenmgm2nfun

Description: The operation of a second degenerate magma is not a function. (Contributed by AV, 21-Aug-2026)

		Ref	Expression
	Hypothesis	degenmgm2.m	$⊢ M = \{⟨{Base}_{ndx}, \{\emptyset, 1_{𝑜}\}⟩, ⟨+_{ndx}, \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}⟩\}$
	Assertion	degenmgm2nfun	$⊢ \neg Fun +_{M}$

Proof

Step	Hyp	Ref	Expression
1		degenmgm2.m	$⊢ M = \{⟨{Base}_{ndx}, \{\emptyset, 1_{𝑜}\}⟩, ⟨+_{ndx}, \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}⟩\}$
2		2oex	$⊢ 2_{𝑜} \in V$
3		opeq2	$⊢ z = 2_{𝑜} \to ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ = ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩$
4	3	eleq1d	$⊢ z = 2_{𝑜} \to (⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \leftrightarrow ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\})$
5	4	anbi2d	$⊢ z = 2_{𝑜} \to ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \leftrightarrow (⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}))$
6		eqeq2	$⊢ z = 2_{𝑜} \to (1_{𝑜} = z \leftrightarrow 1_{𝑜} = 2_{𝑜})$
7	6	necon3bbid	$⊢ z = 2_{𝑜} \to (\neg 1_{𝑜} = z \leftrightarrow 1_{𝑜} \neq 2_{𝑜})$
8	5 7	anbi12d	$⊢ z = 2_{𝑜} \to (((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \land \neg 1_{𝑜} = z) \leftrightarrow ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \land 1_{𝑜} \neq 2_{𝑜}))$
9		opex	$⊢ ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in V$
10	9	tpid2	$⊢ ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}$
11		opex	$⊢ ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩ \in V$
12	11	tpid3	$⊢ ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}$
13	10 12	pm3.2i	$⊢ (⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\})$
14		1one2o	$⊢ 1_{𝑜} \neq 2_{𝑜}$
15	13 14	pm3.2i	$⊢ ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \land 1_{𝑜} \neq 2_{𝑜})$
16	2 8 15	ceqsexv2d	$⊢ \exists z ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \land \neg 1_{𝑜} = z)$
17		opex	$⊢ ⟨1_{𝑜}, 2_{𝑜}⟩ \in V$
18		1oex	$⊢ 1_{𝑜} \in V$
19		opeq12	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to ⟨x, y⟩ = ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩$
20	19	eleq1d	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to (⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \leftrightarrow ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\})$
21		opeq1	$⊢ x = ⟨1_{𝑜}, 2_{𝑜}⟩ \to ⟨x, z⟩ = ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩$
22	21	adantr	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to ⟨x, z⟩ = ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩$
23	22	eleq1d	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to (⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \leftrightarrow ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\})$
24	20 23	anbi12d	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \leftrightarrow (⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}))$
25		eqeq1	$⊢ y = 1_{𝑜} \to (y = z \leftrightarrow 1_{𝑜} = z)$
26	25	adantl	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to (y = z \leftrightarrow 1_{𝑜} = z)$
27	24 26	imbi12d	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to (((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z) \leftrightarrow ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to 1_{𝑜} = z))$
28	27	notbid	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to (\neg ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z) \leftrightarrow \neg ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to 1_{𝑜} = z))$
29		pm4.61	$⊢ \neg ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to 1_{𝑜} = z) \leftrightarrow ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \land \neg 1_{𝑜} = z)$
30	28 29	bitrdi	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to (\neg ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z) \leftrightarrow ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \land \neg 1_{𝑜} = z))$
31	30	exbidv	$⊢ (x = ⟨1_{𝑜}, 2_{𝑜}⟩ \land y = 1_{𝑜}) \to (\exists z \neg ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z) \leftrightarrow \exists z ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \land \neg 1_{𝑜} = z))$
32	17 18 31	spc2ev	$⊢ \exists z ((⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨⟨1_{𝑜}, 2_{𝑜}⟩, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \land \neg 1_{𝑜} = z) \to \exists x \exists y \exists z \neg ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z)$
33	16 32	ax-mp	$⊢ \exists x \exists y \exists z \neg ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z)$
34		exnal	$⊢ \exists z \neg ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z) \leftrightarrow \neg \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z)$
35	34	bicomi	$⊢ \neg \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z) \leftrightarrow \exists z \neg ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z)$
36	35	2exbii	$⊢ \exists x \exists y \neg \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z) \leftrightarrow \exists x \exists y \exists z \neg ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z)$
37	33 36	mpbir	$⊢ \exists x \exists y \neg \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z)$
38		2nalexn	$⊢ \neg \forall x \forall y \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z) \leftrightarrow \exists x \exists y \neg \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z)$
39	37 38	mpbir	$⊢ \neg \forall x \forall y \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z)$
40	39	intnan	$⊢ \neg (Rel \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land \forall x \forall y \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z))$
41		tpex	$⊢ \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \in V$
42	1	grpplusg	$⊢ \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \in V \to \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} = +_{M}$
43	41 42	ax-mp	$⊢ \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} = +_{M}$
44	43	eqcomi	$⊢ +_{M} = \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}$
45	44	funeqi	$⊢ Fun +_{M} \leftrightarrow Fun \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}$
46		dffun4	$⊢ Fun \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \leftrightarrow (Rel \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land \forall x \forall y \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z))$
47	45 46	bitri	$⊢ Fun +_{M} \leftrightarrow (Rel \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land \forall x \forall y \forall z ((⟨x, y⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\} \land ⟨x, z⟩ \in \{⟨⟨1_{𝑜}, 1_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 1_{𝑜}⟩, ⟨⟨1_{𝑜}, 2_{𝑜}⟩, 2_{𝑜}⟩\}) \to y = z))$
48	40 47	mtbir	$⊢ \neg Fun +_{M}$

Metamath Proof Explorer

Theorem degenmgm2nfun

Proof