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

Metamath Proof Explorer

Theorem symgmov2

Description: For a permutation of a set, each element of the set is replaced by an(other) element of the set. (Contributed by AV, 2-Jan-2019)

Ref Expression
Hypothesis symgmov1.p ⊢ P = Base SymGrp ⁡ N
Assertion symgmov2 ⊢ Q ∈ P → ∀ n ∈ N ∃ k ∈ N Q ⁡ k = n

Proof

Step Hyp Ref Expression
1 symgmov1.p ⊢ P = Base SymGrp ⁡ N
2 eqid ⊢ SymGrp ⁡ N = SymGrp ⁡ N
3 2 1 symgbasf1o ⊢ Q ∈ P → Q : N ⟶ 1-1 onto N
4 f1ofo ⊢ Q : N ⟶ 1-1 onto N → Q : N ⟶ onto N
5 foelcdmi ⊢ Q : N ⟶ onto N ∧ n ∈ N → ∃ k ∈ N Q ⁡ k = n
6 5 ralrimiva ⊢ Q : N ⟶ onto N → ∀ n ∈ N ∃ k ∈ N Q ⁡ k = n
7 3 4 6 3syl ⊢ Q ∈ P → ∀ n ∈ N ∃ k ∈ N Q ⁡ k = n