Metamath Proof Explorer

Theorem degenmgm2opdm

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

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

Proof

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