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	⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
	symgpssefmnd.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
Assertion	symgpssefmnd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		symgpssefmnd.m	⊢ 𝑀 = ( EndoFMnd ‘ 𝐴 )
2		symgpssefmnd.g	⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
3		hashgt12el	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 )
4		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
5	2 4	symgbasmap	⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) → 𝑥 ∈ ( 𝐴 ↑_m 𝐴 ) )
6		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
7	1 6	efmndbas	⊢ ( Base ‘ 𝑀 ) = ( 𝐴 ↑_m 𝐴 )
8	5 7	eleqtrrdi	⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
9	8	ssriv	⊢ ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝑀 )
10	9	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( Base ‘ 𝐺 ) ⊆ ( Base ‘ 𝑀 ) )
11		fconst6g	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 )
12	11	adantr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 )
13	12	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 )
14	1 6	elefmndbas	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝑀 ) ↔ ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 ) )
15	14	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝑀 ) ↔ ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ 𝐴 ) )
16	13 15	mpbird	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝑀 ) )
17		fconstg	⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } )
18	17	adantr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } )
19	18	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } )
20		id	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) )
21	20	3expa	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) )
22	21	3adant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) )
23		nf1oconst	⊢ ( ( ( 𝐴 × { 𝑥 } ) : 𝐴 ⟶ { 𝑥 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≠ 𝑦 ) ) → ¬ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 )
24	19 22 23	syl2anc	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ¬ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 )
25	2 4	elsymgbas	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝐺 ) ↔ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 ) )
26	25	notbid	⊢ ( 𝐴 ∈ 𝑉 → ( ¬ ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝐺 ) ↔ ¬ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 ) )
27	26	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( ¬ ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝐺 ) ↔ ¬ ( 𝐴 × { 𝑥 } ) : 𝐴 –1-1-onto→ 𝐴 ) )
28	24 27	mpbird	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ¬ ( 𝐴 × { 𝑥 } ) ∈ ( Base ‘ 𝐺 ) )
29	10 16 28	ssnelpssd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ≠ 𝑦 ) → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) )
30	29	3exp	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ≠ 𝑦 → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) ) ) )
31	30	rexlimdvv	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) ) )
32	31	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 ≠ 𝑦 → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) ) )
33	3 32	mpd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ( Base ‘ 𝐺 ) ⊊ ( Base ‘ 𝑀 ) )

Metamath Proof Explorer

Theorem symgpssefmnd

Proof