Database
BASIC ALGEBRAIC STRUCTURES
Groups
Symmetric groups
Definition and basic properties
symg1hash
Next ⟩
symg1bas
Metamath Proof Explorer
Ascii
Unicode
Theorem
symg1hash
Description:
The symmetric group on a singleton has cardinality
1
.
(Contributed by
AV
, 9-Dec-2018)
Ref
Expression
Hypotheses
symg1bas.1
⊢
G
=
SymGrp
⁡
A
symg1bas.2
⊢
B
=
Base
G
symg1bas.0
⊢
A
=
I
Assertion
symg1hash
⊢
I
∈
V
→
B
=
1
Proof
Step
Hyp
Ref
Expression
1
symg1bas.1
⊢
G
=
SymGrp
⁡
A
2
symg1bas.2
⊢
B
=
Base
G
3
symg1bas.0
⊢
A
=
I
4
snfi
⊢
I
∈
Fin
5
3
4
eqeltri
⊢
A
∈
Fin
6
1
2
symghash
⊢
A
∈
Fin
→
B
=
A
!
7
5
6
ax-mp
⊢
B
=
A
!
8
3
fveq2i
⊢
A
=
I
9
hashsng
⊢
I
∈
V
→
I
=
1
10
8
9
eqtrid
⊢
I
∈
V
→
A
=
1
11
10
fveq2d
⊢
I
∈
V
→
A
!
=
1
!
12
fac1
⊢
1
!
=
1
13
11
12
eqtrdi
⊢
I
∈
V
→
A
!
=
1
14
7
13
eqtrid
⊢
I
∈
V
→
B
=
1