This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⁡ ∅ = ∅