This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symgbasfi

Description: The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018)

Ref Expression
Hypotheses symgbas.1 
|- G = ( SymGrp ` A )
symgbas.2 
|- B = ( Base ` G )
Assertion symgbasfi 
|- ( A e. Fin -> B e. Fin )

Proof

Step Hyp Ref Expression
1 symgbas.1 
 |-  G = ( SymGrp ` A )
2 symgbas.2 
 |-  B = ( Base ` G )
3 mapfi 
 |-  ( ( A e. Fin /\ A e. Fin ) -> ( A ^m A ) e. Fin )
4 3 anidms 
 |-  ( A e. Fin -> ( A ^m A ) e. Fin )
5 1 2 symgbas 
 |-  B = { f | f : A -1-1-onto-> A }
6 f1of 
 |-  ( f : A -1-1-onto-> A -> f : A --> A )
7 6 ss2abi 
 |-  { f | f : A -1-1-onto-> A } C_ { f | f : A --> A }
8 5 7 eqsstri 
 |-  B C_ { f | f : A --> A }
9 mapvalg 
 |-  ( ( A e. Fin /\ A e. Fin ) -> ( A ^m A ) = { f | f : A --> A } )
10 9 anidms 
 |-  ( A e. Fin -> ( A ^m A ) = { f | f : A --> A } )
11 8 10 sseqtrrid 
 |-  ( A e. Fin -> B C_ ( A ^m A ) )
12 4 11 ssfid 
 |-  ( A e. Fin -> B e. Fin )