Theorem mgmb1mgm1

Description: The only magma with a base set consisting of one element is the trivial magma (at least if its operation is an internal binary operation). (Contributed by AV, 23-Jan-2020) (Revised by AV, 7-Feb-2020)

	Ref	Expression
Hypotheses	mgmb1mgm1.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	mgmb1mgm1.p	⊢ + = ( +g ‘ 𝑀 )
Assertion	mgmb1mgm1	⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		mgmb1mgm1.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
2		mgmb1mgm1.p	⊢ + = ( +g ‘ 𝑀 )
3		eqid	⊢ ( +𝑓 ‘ 𝑀 ) = ( +𝑓 ‘ 𝑀 )
4	1 2 3	plusfeq	⊢ ( + Fn ( 𝐵 × 𝐵 ) → ( +𝑓 ‘ 𝑀 ) = + )
5	1 3	mgmplusf	⊢ ( 𝑀 ∈ Mgm → ( +𝑓 ‘ 𝑀 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
6		feq1	⊢ ( ( +𝑓 ‘ 𝑀 ) = + → ( ( +𝑓 ‘ 𝑀 ) : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ↔ + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) )
7	5 6	imbitrid	⊢ ( ( +𝑓 ‘ 𝑀 ) = + → ( 𝑀 ∈ Mgm → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) )
8	4 7	syl	⊢ ( + Fn ( 𝐵 × 𝐵 ) → ( 𝑀 ∈ Mgm → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ) )
9	8	impcom	⊢ ( ( 𝑀 ∈ Mgm ∧ + Fn ( 𝐵 × 𝐵 ) ) → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
10	9	3adant2	⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn ( 𝐵 × 𝐵 ) ) → + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
11		simp2	⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn ( 𝐵 × 𝐵 ) ) → 𝑍 ∈ 𝐵 )
12		intopsn	⊢ ( ( + : ( 𝐵 × 𝐵 ) ⟶ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )
13	10 11 12	syl2anc	⊢ ( ( 𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn ( 𝐵 × 𝐵 ) ) → ( 𝐵 = { 𝑍 } ↔ + = { ⟨ ⟨ 𝑍 , 𝑍 ⟩ , 𝑍 ⟩ } ) )