Metamath Proof Explorer

Theorem symgbas0

Description: The base set of the symmetric group on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Feb-2019)

Ref Expression
Assertion symgbas0 
|- ( Base ` ( SymGrp ` (/) ) ) = { (/) }

Proof

Step Hyp Ref Expression
1 eqid 
 |-  (/) = (/)
2 f1o00 
 |-  ( f : (/) -1-1-onto-> (/) <-> ( f = (/) /\ (/) = (/) ) )
3 1 2 mpbiran2 
 |-  ( f : (/) -1-1-onto-> (/) <-> f = (/) )
4 3 abbii 
 |-  { f | f : (/) -1-1-onto-> (/) } = { f | f = (/) }
5 eqid 
 |-  ( SymGrp ` (/) ) = ( SymGrp ` (/) )
6 eqid 
 |-  ( Base ` ( SymGrp ` (/) ) ) = ( Base ` ( SymGrp ` (/) ) )
7 5 6 symgbas 
 |-  ( Base ` ( SymGrp ` (/) ) ) = { f | f : (/) -1-1-onto-> (/) }
8 df-sn 
 |-  { (/) } = { f | f = (/) }
9 4 7 8 3eqtr4i 
 |-  ( Base ` ( SymGrp ` (/) ) ) = { (/) }