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 
|- M = ( EndoFMnd ` A )
symgpssefmnd.g 
|- G = ( SymGrp ` A )
Assertion symgpssefmnd 
|- ( ( A e. V /\ 1 < ( # ` A ) ) -> ( Base ` G ) C. ( Base ` M ) )

Proof

Step Hyp Ref Expression
1 symgpssefmnd.m 
 |-  M = ( EndoFMnd ` A )
2 symgpssefmnd.g 
 |-  G = ( SymGrp ` A )
3 hashgt12el 
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> E. x e. A E. y e. A x =/= y )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 2 4 symgbasmap 
 |-  ( x e. ( Base ` G ) -> x e. ( A ^m A ) )
6 eqid 
 |-  ( Base ` M ) = ( Base ` M )
7 1 6 efmndbas 
 |-  ( Base ` M ) = ( A ^m A )
8 5 7 eleqtrrdi 
 |-  ( x e. ( Base ` G ) -> x e. ( Base ` M ) )
9 8 ssriv 
 |-  ( Base ` G ) C_ ( Base ` M )
10 9 a1i 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> ( Base ` G ) C_ ( Base ` M ) )
11 fconst6g 
 |-  ( x e. A -> ( A X. { x } ) : A --> A )
12 11 adantr 
 |-  ( ( x e. A /\ y e. A ) -> ( A X. { x } ) : A --> A )
13 12 3ad2ant2 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> ( A X. { x } ) : A --> A )
14 1 6 elefmndbas 
 |-  ( A e. V -> ( ( A X. { x } ) e. ( Base ` M ) <-> ( A X. { x } ) : A --> A ) )
15 14 3ad2ant1 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> ( ( A X. { x } ) e. ( Base ` M ) <-> ( A X. { x } ) : A --> A ) )
16 13 15 mpbird 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> ( A X. { x } ) e. ( Base ` M ) )
17 fconstg 
 |-  ( x e. A -> ( A X. { x } ) : A --> { x } )
18 17 adantr 
 |-  ( ( x e. A /\ y e. A ) -> ( A X. { x } ) : A --> { x } )
19 18 3ad2ant2 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> ( A X. { x } ) : A --> { x } )
20 id 
 |-  ( ( x e. A /\ y e. A /\ x =/= y ) -> ( x e. A /\ y e. A /\ x =/= y ) )
21 20 3expa 
 |-  ( ( ( x e. A /\ y e. A ) /\ x =/= y ) -> ( x e. A /\ y e. A /\ x =/= y ) )
22 21 3adant1 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> ( x e. A /\ y e. A /\ x =/= y ) )
23 nf1oconst 
 |-  ( ( ( A X. { x } ) : A --> { x } /\ ( x e. A /\ y e. A /\ x =/= y ) ) -> -. ( A X. { x } ) : A -1-1-onto-> A )
24 19 22 23 syl2anc 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> -. ( A X. { x } ) : A -1-1-onto-> A )
25 2 4 elsymgbas 
 |-  ( A e. V -> ( ( A X. { x } ) e. ( Base ` G ) <-> ( A X. { x } ) : A -1-1-onto-> A ) )
26 25 notbid 
 |-  ( A e. V -> ( -. ( A X. { x } ) e. ( Base ` G ) <-> -. ( A X. { x } ) : A -1-1-onto-> A ) )
27 26 3ad2ant1 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> ( -. ( A X. { x } ) e. ( Base ` G ) <-> -. ( A X. { x } ) : A -1-1-onto-> A ) )
28 24 27 mpbird 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> -. ( A X. { x } ) e. ( Base ` G ) )
29 10 16 28 ssnelpssd 
 |-  ( ( A e. V /\ ( x e. A /\ y e. A ) /\ x =/= y ) -> ( Base ` G ) C. ( Base ` M ) )
30 29 3exp 
 |-  ( A e. V -> ( ( x e. A /\ y e. A ) -> ( x =/= y -> ( Base ` G ) C. ( Base ` M ) ) ) )
31 30 rexlimdvv 
 |-  ( A e. V -> ( E. x e. A E. y e. A x =/= y -> ( Base ` G ) C. ( Base ` M ) ) )
32 31 adantr 
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( E. x e. A E. y e. A x =/= y -> ( Base ` G ) C. ( Base ` M ) ) )
33 3 32 mpd 
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( Base ` G ) C. ( Base ` M ) )