Theorem symgmov1

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

	Ref	Expression
Hypothesis	symgmov1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
Assertion	symgmov1	⊢ ( 𝑄 ∈ 𝑃 → ∀ 𝑛 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑛 ) = 𝑘 )

Proof

Step	Hyp	Ref	Expression
1		symgmov1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
3	2 1	symgfv	⊢ ( ( 𝑄 ∈ 𝑃 ∧ 𝑛 ∈ 𝑁 ) → ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 )
4		clel5	⊢ ( ( 𝑄 ‘ 𝑛 ) ∈ 𝑁 ↔ ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑛 ) = 𝑘 )
5	3 4	sylib	⊢ ( ( 𝑄 ∈ 𝑃 ∧ 𝑛 ∈ 𝑁 ) → ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑛 ) = 𝑘 )
6	5	ralrimiva	⊢ ( 𝑄 ∈ 𝑃 → ∀ 𝑛 ∈ 𝑁 ∃ 𝑘 ∈ 𝑁 ( 𝑄 ‘ 𝑛 ) = 𝑘 )