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 e. P -> A. n e. N E. k e. 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 e. 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 e. N ) -> E. k e. N ( Q ` k ) = n )
6	5	ralrimiva	|- ( Q : N -onto-> N -> A. n e. N E. k e. N ( Q ` k ) = n )
7	3 4 6	3syl	|- ( Q e. P -> A. n e. N E. k e. N ( Q ` k ) = n )