Theorem degenmgm

Description: A degenerate magma: although the operation is not defined for all pairs of elements of the base set ( ( (/) ( +gM ) 1o ) and ( (/) ( +gM ) (/) ) are not defined, and therefore are (/) by definition, which is contained in the base set), and its domain is not (a subset of) the base set ( 2o is in the domain of the operation, but not in the base set) , the structure M is still a magma according to our definition. (Contributed by AV, 18-Aug-2026)

	Ref	Expression
Hypothesis	degenmgm.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1o } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ⟩ }
Assertion	degenmgm	⊢ 𝑀 ∈ Mgm

Proof

Step	Hyp	Ref	Expression
1		degenmgm.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1o } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ⟩ }
2		0ex	⊢ ∅ ∈ V
3	2	prid1	⊢ ∅ ∈ { ∅ , 1o }
4	3 3	pm3.2i	⊢ ( ∅ ∈ { ∅ , 1o } ∧ ∅ ∈ { ∅ , 1o } )
5		1oelpr	⊢ 1o ∈ { ∅ , 1o }
6	5 5	pm3.2i	⊢ ( 1o ∈ { ∅ , 1o } ∧ 1o ∈ { ∅ , 1o } )
7	4 6	pm3.2i	⊢ ( ( ∅ ∈ { ∅ , 1o } ∧ ∅ ∈ { ∅ , 1o } ) ∧ ( 1o ∈ { ∅ , 1o } ∧ 1o ∈ { ∅ , 1o } ) )
8		1oex	⊢ 1o ∈ V
9		oveq1	⊢ ( 𝑥 = ∅ → ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) = ( ∅ { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) )
10		df-ov	⊢ ( ∅ { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) = ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ )
11	9 10	eqtrdi	⊢ ( 𝑥 = ∅ → ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) = ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) )
12	11	eleq1d	⊢ ( 𝑥 = ∅ → ( ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) ∈ { ∅ , 1o } ↔ ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) ∈ { ∅ , 1o } ) )
13	12	ralbidv	⊢ ( 𝑥 = ∅ → ( ∀ 𝑦 ∈ { ∅ , 1o } ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) ∈ { ∅ , 1o } ↔ ∀ 𝑦 ∈ { ∅ , 1o } ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) ∈ { ∅ , 1o } ) )
14		oveq1	⊢ ( 𝑥 = 1o → ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) = ( 1o { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) )
15		df-ov	⊢ ( 1o { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) = ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ )
16	14 15	eqtrdi	⊢ ( 𝑥 = 1o → ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) = ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) )
17	16	eleq1d	⊢ ( 𝑥 = 1o → ( ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) ∈ { ∅ , 1o } ↔ ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) ∈ { ∅ , 1o } ) )
18	17	ralbidv	⊢ ( 𝑥 = 1o → ( ∀ 𝑦 ∈ { ∅ , 1o } ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) ∈ { ∅ , 1o } ↔ ∀ 𝑦 ∈ { ∅ , 1o } ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) ∈ { ∅ , 1o } ) )
19	2 8 13 18	ralpr	⊢ ( ∀ 𝑥 ∈ { ∅ , 1o } ∀ 𝑦 ∈ { ∅ , 1o } ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) ∈ { ∅ , 1o } ↔ ( ∀ 𝑦 ∈ { ∅ , 1o } ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) ∈ { ∅ , 1o } ∧ ∀ 𝑦 ∈ { ∅ , 1o } ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) ∈ { ∅ , 1o } ) )
20		opeq2	⊢ ( 𝑦 = ∅ → ⟨ ∅ , 𝑦 ⟩ = ⟨ ∅ , ∅ ⟩ )
21	20	fveq2d	⊢ ( 𝑦 = ∅ → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) = ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , ∅ ⟩ ) )
22		1n0	⊢ 1o ≠ ∅
23	22	necomi	⊢ ∅ ≠ 1o
24	23	orci	⊢ ( ∅ ≠ 1o ∨ ∅ ≠ 1o )
25	2 2	opthne	⊢ ( ⟨ ∅ , ∅ ⟩ ≠ ⟨ 1o , 1o ⟩ ↔ ( ∅ ≠ 1o ∨ ∅ ≠ 1o ) )
26	24 25	mpbir	⊢ ⟨ ∅ , ∅ ⟩ ≠ ⟨ 1o , 1o ⟩
27	23	orci	⊢ ( ∅ ≠ 1o ∨ ∅ ≠ 2o )
28	2 2	opthne	⊢ ( ⟨ ∅ , ∅ ⟩ ≠ ⟨ 1o , 2o ⟩ ↔ ( ∅ ≠ 1o ∨ ∅ ≠ 2o ) )
29	27 28	mpbir	⊢ ⟨ ∅ , ∅ ⟩ ≠ ⟨ 1o , 2o ⟩
30	23	orci	⊢ ( ∅ ≠ 1o ∨ ∅ ≠ ∅ )
31	2 2	opthne	⊢ ( ⟨ ∅ , ∅ ⟩ ≠ ⟨ 1o , ∅ ⟩ ↔ ( ∅ ≠ 1o ∨ ∅ ≠ ∅ ) )
32	30 31	mpbir	⊢ ⟨ ∅ , ∅ ⟩ ≠ ⟨ 1o , ∅ ⟩
33		opex	⊢ ⟨ ∅ , ∅ ⟩ ∈ V
34	8 8 8 33	fvtp0	⊢ ( ( ⟨ ∅ , ∅ ⟩ ≠ ⟨ 1o , 1o ⟩ ∧ ⟨ ∅ , ∅ ⟩ ≠ ⟨ 1o , 2o ⟩ ∧ ⟨ ∅ , ∅ ⟩ ≠ ⟨ 1o , ∅ ⟩ ) → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , ∅ ⟩ ) = ∅ )
35	26 29 32 34	mp3an	⊢ ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , ∅ ⟩ ) = ∅
36	21 35	eqtrdi	⊢ ( 𝑦 = ∅ → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) = ∅ )
37	36	eleq1d	⊢ ( 𝑦 = ∅ → ( ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) ∈ { ∅ , 1o } ↔ ∅ ∈ { ∅ , 1o } ) )
38		opeq2	⊢ ( 𝑦 = 1o → ⟨ ∅ , 𝑦 ⟩ = ⟨ ∅ , 1o ⟩ )
39	38	fveq2d	⊢ ( 𝑦 = 1o → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) = ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 1o ⟩ ) )
40	23	orci	⊢ ( ∅ ≠ 1o ∨ 1o ≠ 1o )
41	2 8	opthne	⊢ ( ⟨ ∅ , 1o ⟩ ≠ ⟨ 1o , 1o ⟩ ↔ ( ∅ ≠ 1o ∨ 1o ≠ 1o ) )
42	40 41	mpbir	⊢ ⟨ ∅ , 1o ⟩ ≠ ⟨ 1o , 1o ⟩
43	23	orci	⊢ ( ∅ ≠ 1o ∨ 1o ≠ 2o )
44	2 8	opthne	⊢ ( ⟨ ∅ , 1o ⟩ ≠ ⟨ 1o , 2o ⟩ ↔ ( ∅ ≠ 1o ∨ 1o ≠ 2o ) )
45	43 44	mpbir	⊢ ⟨ ∅ , 1o ⟩ ≠ ⟨ 1o , 2o ⟩
46	22	olci	⊢ ( ∅ ≠ 1o ∨ 1o ≠ ∅ )
47	2 8	opthne	⊢ ( ⟨ ∅ , 1o ⟩ ≠ ⟨ 1o , ∅ ⟩ ↔ ( ∅ ≠ 1o ∨ 1o ≠ ∅ ) )
48	46 47	mpbir	⊢ ⟨ ∅ , 1o ⟩ ≠ ⟨ 1o , ∅ ⟩
49		opex	⊢ ⟨ ∅ , 1o ⟩ ∈ V
50	8 8 8 49	fvtp0	⊢ ( ( ⟨ ∅ , 1o ⟩ ≠ ⟨ 1o , 1o ⟩ ∧ ⟨ ∅ , 1o ⟩ ≠ ⟨ 1o , 2o ⟩ ∧ ⟨ ∅ , 1o ⟩ ≠ ⟨ 1o , ∅ ⟩ ) → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 1o ⟩ ) = ∅ )
51	42 45 48 50	mp3an	⊢ ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 1o ⟩ ) = ∅
52	39 51	eqtrdi	⊢ ( 𝑦 = 1o → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) = ∅ )
53	52	eleq1d	⊢ ( 𝑦 = 1o → ( ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) ∈ { ∅ , 1o } ↔ ∅ ∈ { ∅ , 1o } ) )
54	2 8 37 53	ralpr	⊢ ( ∀ 𝑦 ∈ { ∅ , 1o } ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) ∈ { ∅ , 1o } ↔ ( ∅ ∈ { ∅ , 1o } ∧ ∅ ∈ { ∅ , 1o } ) )
55		opeq2	⊢ ( 𝑦 = ∅ → ⟨ 1o , 𝑦 ⟩ = ⟨ 1o , ∅ ⟩ )
56	55	fveq2d	⊢ ( 𝑦 = ∅ → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) = ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , ∅ ⟩ ) )
57	22	olci	⊢ ( 1o ≠ 1o ∨ 1o ≠ ∅ )
58	8 8	opthne	⊢ ( ⟨ 1o , 1o ⟩ ≠ ⟨ 1o , ∅ ⟩ ↔ ( 1o ≠ 1o ∨ 1o ≠ ∅ ) )
59	57 58	mpbir	⊢ ⟨ 1o , 1o ⟩ ≠ ⟨ 1o , ∅ ⟩
60		2on0	⊢ 2o ≠ ∅
61	60	olci	⊢ ( 1o ≠ 1o ∨ 2o ≠ ∅ )
62		2oex	⊢ 2o ∈ V
63	8 62	opthne	⊢ ( ⟨ 1o , 2o ⟩ ≠ ⟨ 1o , ∅ ⟩ ↔ ( 1o ≠ 1o ∨ 2o ≠ ∅ ) )
64	61 63	mpbir	⊢ ⟨ 1o , 2o ⟩ ≠ ⟨ 1o , ∅ ⟩
65		opex	⊢ ⟨ 1o , ∅ ⟩ ∈ V
66	65 8	fvtp3	⊢ ( ( ⟨ 1o , 1o ⟩ ≠ ⟨ 1o , ∅ ⟩ ∧ ⟨ 1o , 2o ⟩ ≠ ⟨ 1o , ∅ ⟩ ) → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , ∅ ⟩ ) = 1o )
67	59 64 66	mp2an	⊢ ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , ∅ ⟩ ) = 1o
68	56 67	eqtrdi	⊢ ( 𝑦 = ∅ → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) = 1o )
69	68	eleq1d	⊢ ( 𝑦 = ∅ → ( ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) ∈ { ∅ , 1o } ↔ 1o ∈ { ∅ , 1o } ) )
70		opeq2	⊢ ( 𝑦 = 1o → ⟨ 1o , 𝑦 ⟩ = ⟨ 1o , 1o ⟩ )
71	70	fveq2d	⊢ ( 𝑦 = 1o → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) = ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 1o ⟩ ) )
72		1one2o	⊢ 1o ≠ 2o
73	72	olci	⊢ ( 1o ≠ 1o ∨ 1o ≠ 2o )
74	8 8	opthne	⊢ ( ⟨ 1o , 1o ⟩ ≠ ⟨ 1o , 2o ⟩ ↔ ( 1o ≠ 1o ∨ 1o ≠ 2o ) )
75	73 74	mpbir	⊢ ⟨ 1o , 1o ⟩ ≠ ⟨ 1o , 2o ⟩
76		opex	⊢ ⟨ 1o , 1o ⟩ ∈ V
77	76 8	fvtp1	⊢ ( ( ⟨ 1o , 1o ⟩ ≠ ⟨ 1o , 2o ⟩ ∧ ⟨ 1o , 1o ⟩ ≠ ⟨ 1o , ∅ ⟩ ) → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 1o ⟩ ) = 1o )
78	75 59 77	mp2an	⊢ ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 1o ⟩ ) = 1o
79	71 78	eqtrdi	⊢ ( 𝑦 = 1o → ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) = 1o )
80	79	eleq1d	⊢ ( 𝑦 = 1o → ( ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) ∈ { ∅ , 1o } ↔ 1o ∈ { ∅ , 1o } ) )
81	2 8 69 80	ralpr	⊢ ( ∀ 𝑦 ∈ { ∅ , 1o } ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) ∈ { ∅ , 1o } ↔ ( 1o ∈ { ∅ , 1o } ∧ 1o ∈ { ∅ , 1o } ) )
82	54 81	anbi12i	⊢ ( ( ∀ 𝑦 ∈ { ∅ , 1o } ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ ∅ , 𝑦 ⟩ ) ∈ { ∅ , 1o } ∧ ∀ 𝑦 ∈ { ∅ , 1o } ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ‘ ⟨ 1o , 𝑦 ⟩ ) ∈ { ∅ , 1o } ) ↔ ( ( ∅ ∈ { ∅ , 1o } ∧ ∅ ∈ { ∅ , 1o } ) ∧ ( 1o ∈ { ∅ , 1o } ∧ 1o ∈ { ∅ , 1o } ) ) )
83	19 82	bitri	⊢ ( ∀ 𝑥 ∈ { ∅ , 1o } ∀ 𝑦 ∈ { ∅ , 1o } ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) ∈ { ∅ , 1o } ↔ ( ( ∅ ∈ { ∅ , 1o } ∧ ∅ ∈ { ∅ , 1o } ) ∧ ( 1o ∈ { ∅ , 1o } ∧ 1o ∈ { ∅ , 1o } ) ) )
84	7 83	mpbir	⊢ ∀ 𝑥 ∈ { ∅ , 1o } ∀ 𝑦 ∈ { ∅ , 1o } ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) ∈ { ∅ , 1o }
85		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
86	1 85	degenmgmbas	⊢ ( Base ‘ 𝑀 ) = { ∅ , 1o }
87	86	eqcomi	⊢ { ∅ , 1o } = ( Base ‘ 𝑀 )
88		tpex	⊢ { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ∈ V
89	1	grpplusg	⊢ ( { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ∈ V → { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } = ( +g ‘ 𝑀 ) )
90	88 89	ax-mp	⊢ { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } = ( +g ‘ 𝑀 )
91	87 90	ismgmn0	⊢ ( ∅ ∈ { ∅ , 1o } → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ { ∅ , 1o } ∀ 𝑦 ∈ { ∅ , 1o } ( 𝑥 { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } 𝑦 ) ∈ { ∅ , 1o } ) )
92	84 91	mpbiri	⊢ ( ∅ ∈ { ∅ , 1o } → 𝑀 ∈ Mgm )
93	3 92	ax-mp	⊢ 𝑀 ∈ Mgm