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 ( 𝑓 : ∅ –1-1-onto→ ∅ ↔ ( 𝑓 = ∅ ∧ ∅ = ∅ ) )
3 1 2 mpbiran2 ( 𝑓 : ∅ –1-1-onto→ ∅ ↔ 𝑓 = ∅ )
4 3 abbii { 𝑓𝑓 : ∅ –1-1-onto→ ∅ } = { 𝑓𝑓 = ∅ }
5 eqid ( SymGrp ‘ ∅ ) = ( SymGrp ‘ ∅ )
6 eqid ( Base ‘ ( SymGrp ‘ ∅ ) ) = ( Base ‘ ( SymGrp ‘ ∅ ) )
7 5 6 symgbas ( Base ‘ ( SymGrp ‘ ∅ ) ) = { 𝑓𝑓 : ∅ –1-1-onto→ ∅ }
8 df-sn { ∅ } = { 𝑓𝑓 = ∅ }
9 4 7 8 3eqtr4i ( Base ‘ ( SymGrp ‘ ∅ ) ) = { ∅ }