Theorem degenmgm2

Description: A degenerate magma: although the operation is not defined for all pairs of elements of the base set, and its domain is not (a subset of) the base set, and the operation is not a function (see degenmgm2nfun ), the structure M is still a magma according to our definition. (Contributed by AV, 21-Aug-2026)

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

Proof

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