Metamath Proof Explorer


Theorem 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 ‘ 𝑀 ) )