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 ‘ ∅ ) ) = { ∅ }