Database
BASIC ALGEBRAIC STRUCTURES
Groups
Symmetric groups
Definition and basic properties
permsetex
Next ⟩
symgbas
Metamath Proof Explorer
Ascii
Unicode
Theorem
permsetex
Description:
The set of permutations of a set
A
exists.
(Contributed by
AV
, 30-Mar-2024)
Ref
Expression
Assertion
permsetex
⊢
A
∈
V
→
f
|
f
:
A
⟶
1-1 onto
A
∈
V
Proof
Step
Hyp
Ref
Expression
1
mapex
⊢
A
∈
V
∧
A
∈
V
→
f
|
f
:
A
⟶
A
∈
V
2
1
anidms
⊢
A
∈
V
→
f
|
f
:
A
⟶
A
∈
V
3
f1of
⊢
f
:
A
⟶
1-1 onto
A
→
f
:
A
⟶
A
4
3
ss2abi
⊢
f
|
f
:
A
⟶
1-1 onto
A
⊆
f
|
f
:
A
⟶
A
5
4
a1i
⊢
A
∈
V
→
f
|
f
:
A
⟶
1-1 onto
A
⊆
f
|
f
:
A
⟶
A
6
2
5
ssexd
⊢
A
∈
V
→
f
|
f
:
A
⟶
1-1 onto
A
∈
V