symgpssefmnd

Description: For a set A with more than one element, the symmetric group on A is a proper subset of the monoid of endofunctions on A . (Contributed by AV, 31-Mar-2024)

	Ref	Expression
Hypotheses	symgpssefmnd.m	No typesetting found for \|- M = ( EndoFMnd ` A ) with typecode \|-
	symgpssefmnd.g	$⊢ G = SymGrp (A)$
Assertion	symgpssefmnd	$⊢ (A \in V \land 1 < \|A\|) \to {Base}_{G} \subset {Base}_{M}$

Proof

Step	Hyp	Ref	Expression
1		symgpssefmnd.m	Could not format M = ( EndoFMnd ` A ) : No typesetting found for \|- M = ( EndoFMnd ` A ) with typecode \|-
2		symgpssefmnd.g	$⊢ G = SymGrp (A)$
3		hashgt12el	$⊢ (A \in V \land 1 < \|A\|) \to \exists x \in A \exists y \in A x \neq y$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5	2 4	symgbasmap	$⊢ x \in {Base}_{G} \to x \in (A^{A})$
6		eqid	$⊢ {Base}_{M} = {Base}_{M}$
7	1 6	efmndbas	$⊢ {Base}_{M} = A^{A}$
8	5 7	eleqtrrdi	$⊢ x \in {Base}_{G} \to x \in {Base}_{M}$
9	8	ssriv	$⊢ {Base}_{G} \subseteq {Base}_{M}$
10	9	a1i	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to {Base}_{G} \subseteq {Base}_{M}$
11		fconst6g	$⊢ x \in A \to (A \times \{x\}) : A ⟶ A$
12	11	adantr	$⊢ (x \in A \land y \in A) \to (A \times \{x\}) : A ⟶ A$
13	12	3ad2ant2	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to (A \times \{x\}) : A ⟶ A$
14	1 6	elefmndbas	$⊢ A \in V \to (A \times \{x\} \in {Base}_{M} \leftrightarrow (A \times \{x\}) : A ⟶ A)$
15	14	3ad2ant1	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to (A \times \{x\} \in {Base}_{M} \leftrightarrow (A \times \{x\}) : A ⟶ A)$
16	13 15	mpbird	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to A \times \{x\} \in {Base}_{M}$
17		fconstg	$⊢ x \in A \to (A \times \{x\}) : A ⟶ \{x\}$
18	17	adantr	$⊢ (x \in A \land y \in A) \to (A \times \{x\}) : A ⟶ \{x\}$
19	18	3ad2ant2	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to (A \times \{x\}) : A ⟶ \{x\}$
20		id	$⊢ (x \in A \land y \in A \land x \neq y) \to (x \in A \land y \in A \land x \neq y)$
21	20	3expa	$⊢ ((x \in A \land y \in A) \land x \neq y) \to (x \in A \land y \in A \land x \neq y)$
22	21	3adant1	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to (x \in A \land y \in A \land x \neq y)$
23		nf1oconst	$⊢ ((A \times \{x\}) : A ⟶ \{x\} \land (x \in A \land y \in A \land x \neq y)) \to \neg (A \times \{x\}) : A \underset{1-1 onto}{⟶} A$
24	19 22 23	syl2anc	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to \neg (A \times \{x\}) : A \underset{1-1 onto}{⟶} A$
25	2 4	elsymgbas	$⊢ A \in V \to (A \times \{x\} \in {Base}_{G} \leftrightarrow (A \times \{x\}) : A \underset{1-1 onto}{⟶} A)$
26	25	notbid	$⊢ A \in V \to (\neg A \times \{x\} \in {Base}_{G} \leftrightarrow \neg (A \times \{x\}) : A \underset{1-1 onto}{⟶} A)$
27	26	3ad2ant1	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to (\neg A \times \{x\} \in {Base}_{G} \leftrightarrow \neg (A \times \{x\}) : A \underset{1-1 onto}{⟶} A)$
28	24 27	mpbird	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to \neg A \times \{x\} \in {Base}_{G}$
29	10 16 28	ssnelpssd	$⊢ (A \in V \land (x \in A \land y \in A) \land x \neq y) \to {Base}_{G} \subset {Base}_{M}$
30	29	3exp	$⊢ A \in V \to ((x \in A \land y \in A) \to (x \neq y \to {Base}_{G} \subset {Base}_{M}))$
31	30	rexlimdvv	$⊢ A \in V \to (\exists x \in A \exists y \in A x \neq y \to {Base}_{G} \subset {Base}_{M})$
32	31	adantr	$⊢ (A \in V \land 1 < \|A\|) \to (\exists x \in A \exists y \in A x \neq y \to {Base}_{G} \subset {Base}_{M})$
33	3 32	mpd	$⊢ (A \in V \land 1 < \|A\|) \to {Base}_{G} \subset {Base}_{M}$

Metamath Proof Explorer

Theorem symgpssefmnd

Proof