Metamath Proof Explorer

Theorem degenmgmopdm

Description: The domain of the operation of a degenerate magma. (Contributed by AV, 18-Aug-2026)

		Ref	Expression
	Hypothesis	degenmgm.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1_o } ⟩ , ⟨ ( +_g ‘ ndx ) , { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , ∅ ⟩ , 1_o ⟩ } ⟩ }
	Assertion	degenmgmopdm	⊢ dom ( +_g ‘ 𝑀 ) = ( { 1_o } × { ∅ , 1_o , 2_o } )

Proof

Step	Hyp	Ref	Expression
1		degenmgm.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , { ∅ , 1_o } ⟩ , ⟨ ( +_g ‘ ndx ) , { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , ∅ ⟩ , 1_o ⟩ } ⟩ }
2		1oex	⊢ 1_o ∈ V
3	2 2 2	dmtpop	⊢ dom { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , ∅ ⟩ , 1_o ⟩ } = { ⟨ 1_o , 1_o ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ 1_o , ∅ ⟩ }
4		tpex	⊢ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , ∅ ⟩ , 1_o ⟩ } ∈ V
5	1	grpplusg	⊢ ( { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , ∅ ⟩ , 1_o ⟩ } ∈ V → { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , ∅ ⟩ , 1_o ⟩ } = ( +_g ‘ 𝑀 ) )
6	4 5	ax-mp	⊢ { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , ∅ ⟩ , 1_o ⟩ } = ( +_g ‘ 𝑀 )
7	6	eqcomi	⊢ ( +_g ‘ 𝑀 ) = { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , ∅ ⟩ , 1_o ⟩ }
8	7	dmeqi	⊢ dom ( +_g ‘ 𝑀 ) = dom { ⟨ ⟨ 1_o , 1_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , 2_o ⟩ , 1_o ⟩ , ⟨ ⟨ 1_o , ∅ ⟩ , 1_o ⟩ }
9		0ex	⊢ ∅ ∈ V
10		2oex	⊢ 2_o ∈ V
11		xpsntpg	⊢ ( ( ( 1_o ∈ V ∧ ∅ ∈ V ) ∧ ( 1_o ∈ V ∧ 2_o ∈ V ) ) → ( { 1_o } × { ∅ , 1_o , 2_o } ) = { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 1_o ⟩ , ⟨ 1_o , 2_o ⟩ } )
12	2 9 2 10 11	mp4an	⊢ ( { 1_o } × { ∅ , 1_o , 2_o } ) = { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 1_o ⟩ , ⟨ 1_o , 2_o ⟩ }
13		tprot	⊢ { ⟨ 1_o , ∅ ⟩ , ⟨ 1_o , 1_o ⟩ , ⟨ 1_o , 2_o ⟩ } = { ⟨ 1_o , 1_o ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ 1_o , ∅ ⟩ }
14	12 13	eqtri	⊢ ( { 1_o } × { ∅ , 1_o , 2_o } ) = { ⟨ 1_o , 1_o ⟩ , ⟨ 1_o , 2_o ⟩ , ⟨ 1_o , ∅ ⟩ }
15	3 8 14	3eqtr4i	⊢ dom ( +_g ‘ 𝑀 ) = ( { 1_o } × { ∅ , 1_o , 2_o } )