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	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(\varnothing \right)}=\left\{\varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\varnothing =\varnothing$$
2		f1o00	$$⊢f:\varnothing \underset{1-1\; onto}{⟶}\varnothing \leftrightarrow \left(f=\varnothing \wedge \varnothing =\varnothing \right)$$
3	1 2	mpbiran2	$$⊢f:\varnothing \underset{1-1\; onto}{⟶}\varnothing \leftrightarrow f=\varnothing$$
4	3	abbii	$$⊢\left\{f|f:\varnothing \underset{1-1\; onto}{⟶}\varnothing \right\}=\left\{f|f=\varnothing \right\}$$
5		eqid	$$⊢\mathrm{SymGrp}\left(\varnothing \right)=\mathrm{SymGrp}\left(\varnothing \right)$$
6		eqid	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(\varnothing \right)}={\mathrm{Base}}_{\mathrm{SymGrp}\left(\varnothing \right)}$$
7	5 6	symgbas	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(\varnothing \right)}=\left\{f|f:\varnothing \underset{1-1\; onto}{⟶}\varnothing \right\}$$
8		df-sn	$$⊢\left\{\varnothing \right\}=\left\{f|f=\varnothing \right\}$$
9	4 7 8	3eqtr4i	$$⊢{\mathrm{Base}}_{\mathrm{SymGrp}\left(\varnothing \right)}=\left\{\varnothing \right\}$$