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	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
Assertion	symgmov2	⊢ ( 𝑄 ∈ 𝑃 → ∀ 𝑛 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑛 )

Proof

Step	Hyp	Ref	Expression
1		symgmov1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
3	2 1	symgbasf1o	⊢ ( 𝑄 ∈ 𝑃 → 𝑄 : 𝑁 –1-1-onto→ 𝑁 )
4		f1ofo	⊢ ( 𝑄 : 𝑁 –1-1-onto→ 𝑁 → 𝑄 : 𝑁 –onto→ 𝑁 )
5		foelcdmi	⊢ ( ( 𝑄 : 𝑁 –onto→ 𝑁 ∧ 𝑛 ∈ 𝑁 ) → ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑛 )
6	5	ralrimiva	⊢ ( 𝑄 : 𝑁 –onto→ 𝑁 → ∀ 𝑛 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑛 )
7	3 4 6	3syl	⊢ ( 𝑄 ∈ 𝑃 → ∀ 𝑛 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑘 ) = 𝑛 )