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 ` (/) ) ) = { (/) }