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	|- B = ( Base ` M )
	mgmb1mgm1.p	|- .+ = ( +g ` M )
Assertion	mgmb1mgm1	|- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )

Proof

Step	Hyp	Ref	Expression
1		mgmb1mgm1.b	|- B = ( Base ` M )
2		mgmb1mgm1.p	|- .+ = ( +g ` M )
3		eqid	|- ( +f ` M ) = ( +f ` M )
4	1 2 3	plusfeq	|- ( .+ Fn ( B X. B ) -> ( +f ` M ) = .+ )
5	1 3	mgmplusf	|- ( M e. Mgm -> ( +f ` M ) : ( B X. B ) --> B )
6		feq1	|- ( ( +f ` M ) = .+ -> ( ( +f ` M ) : ( B X. B ) --> B <-> .+ : ( B X. B ) --> B ) )
7	5 6	imbitrid	|- ( ( +f ` M ) = .+ -> ( M e. Mgm -> .+ : ( B X. B ) --> B ) )
8	4 7	syl	|- ( .+ Fn ( B X. B ) -> ( M e. Mgm -> .+ : ( B X. B ) --> B ) )
9	8	impcom	|- ( ( M e. Mgm /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) --> B )
10	9	3adant2	|- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> .+ : ( B X. B ) --> B )
11		simp2	|- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> Z e. B )
12		intopsn	|- ( ( .+ : ( B X. B ) --> B /\ Z e. B ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )
13	10 11 12	syl2anc	|- ( ( M e. Mgm /\ Z e. B /\ .+ Fn ( B X. B ) ) -> ( B = { Z } <-> .+ = { <. <. Z , Z >. , Z >. } ) )