Metamath Proof Explorer

Theorem 0symgefmndeq

Description: The symmetric group on the empty set is identical with the monoid of endofunctions on the empty set. (Contributed by AV, 30-Mar-2024)

Ref Expression
Assertion 0symgefmndeq ⊢ EndoFMnd ⁡ ∅ = SymGrp ⁡ ∅

Proof

Step Hyp Ref Expression
1 ssid ⊢ ∅ ⊆ ∅
2 fvex ⊢ EndoFMnd ⁡ ∅ ∈ V
3 p0ex ⊢ ∅ ∈ V
4 eqid ⊢ SymGrp ⁡ ∅ = SymGrp ⁡ ∅
5 symgbas0 ⊢ Base SymGrp ⁡ ∅ = ∅
6 5 eqcomi ⊢ ∅ = Base SymGrp ⁡ ∅
7 eqid ⊢ EndoFMnd ⁡ ∅ = EndoFMnd ⁡ ∅
8 4 6 7 symgressbas ⊢ SymGrp ⁡ ∅ = EndoFMnd ⁡ ∅ ↾ 𝑠 ∅
9 efmndbas0 ⊢ Base EndoFMnd ⁡ ∅ = ∅
10 9 eqcomi ⊢ ∅ = Base EndoFMnd ⁡ ∅
11 8 10 ressid2 ⊢ ∅ ⊆ ∅ ∧ EndoFMnd ⁡ ∅ ∈ V ∧ ∅ ∈ V → SymGrp ⁡ ∅ = EndoFMnd ⁡ ∅
12 1 2 3 11 mp3an ⊢ SymGrp ⁡ ∅ = EndoFMnd ⁡ ∅
13 12 eqcomi ⊢ EndoFMnd ⁡ ∅ = SymGrp ⁡ ∅