Theorem degenmgmnfn

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

	Ref	Expression
Hypotheses	degenmgm.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1o } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ⟩ }
	degenmgmbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
Assertion	degenmgmnfn	⊢ ¬ ( +g ‘ 𝑀 ) Fn ( 𝐵 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		degenmgm.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1o } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 1o , 1o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , 2o ⟩ , 1o ⟩ , ⟨ ⟨ 1o , ∅ ⟩ , 1o ⟩ } ⟩ }
2		degenmgmbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
3		0ex	⊢ ∅ ∈ V
4		1oex	⊢ 1o ∈ V
5		1n0	⊢ 1o ≠ ∅
6	5	necomi	⊢ ∅ ≠ 1o
7		prnesn	⊢ ( ( ∅ ∈ V ∧ 1o ∈ V ∧ ∅ ≠ 1o ) → { ∅ , 1o } ≠ { 1o } )
8	3 4 6 7	mp3an	⊢ { ∅ , 1o } ≠ { 1o }
9	8	nesymi	⊢ ¬ { 1o } = { ∅ , 1o }
10	9	intnanr	⊢ ¬ ( { 1o } = { ∅ , 1o } ∧ { ∅ , 1o , 2o } = { ∅ , 1o } )
11	4	snnz	⊢ { 1o } ≠ ∅
12	3	tpnz	⊢ { ∅ , 1o , 2o } ≠ ∅
13		xp11	⊢ ( ( { 1o } ≠ ∅ ∧ { ∅ , 1o , 2o } ≠ ∅ ) → ( ( { 1o } × { ∅ , 1o , 2o } ) = ( { ∅ , 1o } × { ∅ , 1o } ) ↔ ( { 1o } = { ∅ , 1o } ∧ { ∅ , 1o , 2o } = { ∅ , 1o } ) ) )
14	11 12 13	mp2an	⊢ ( ( { 1o } × { ∅ , 1o , 2o } ) = ( { ∅ , 1o } × { ∅ , 1o } ) ↔ ( { 1o } = { ∅ , 1o } ∧ { ∅ , 1o , 2o } = { ∅ , 1o } ) )
15	10 14	mtbir	⊢ ¬ ( { 1o } × { ∅ , 1o , 2o } ) = ( { ∅ , 1o } × { ∅ , 1o } )
16	1	degenmgmopdm	⊢ dom ( +g ‘ 𝑀 ) = ( { 1o } × { ∅ , 1o , 2o } )
17	1 2	degenmgmbas	⊢ 𝐵 = { ∅ , 1o }
18	17 17	xpeq12i	⊢ ( 𝐵 × 𝐵 ) = ( { ∅ , 1o } × { ∅ , 1o } )
19	16 18	eqeq12i	⊢ ( dom ( +g ‘ 𝑀 ) = ( 𝐵 × 𝐵 ) ↔ ( { 1o } × { ∅ , 1o , 2o } ) = ( { ∅ , 1o } × { ∅ , 1o } ) )
20	15 19	mtbir	⊢ ¬ dom ( +g ‘ 𝑀 ) = ( 𝐵 × 𝐵 )
21	20	intnan	⊢ ¬ ( Fun ( +g ‘ 𝑀 ) ∧ dom ( +g ‘ 𝑀 ) = ( 𝐵 × 𝐵 ) )
22		df-fn	⊢ ( ( +g ‘ 𝑀 ) Fn ( 𝐵 × 𝐵 ) ↔ ( Fun ( +g ‘ 𝑀 ) ∧ dom ( +g ‘ 𝑀 ) = ( 𝐵 × 𝐵 ) ) )
23	21 22	mtbir	⊢ ¬ ( +g ‘ 𝑀 ) Fn ( 𝐵 × 𝐵 )