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