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	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
Assertion	symgmov1	$$⊢Q\in P\to \forall n\in N\exists k\in NQ\left(n\right)=k$$

Proof

Step	Hyp	Ref	Expression
1		symgmov1.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
2		eqid	$$⊢\mathrm{SymGrp}\left(N\right)=\mathrm{SymGrp}\left(N\right)$$
3	2 1	symgfv	$$⊢\left(Q\in P\wedge n\in N\right)\to Q\left(n\right)\in N$$
4		clel5	$$⊢Q\left(n\right)\in N\leftrightarrow \exists k\in NQ\left(n\right)=k$$
5	3 4	sylib	$$⊢\left(Q\in P\wedge n\in N\right)\to \exists k\in NQ\left(n\right)=k$$
6	5	ralrimiva	$$⊢Q\in P\to \forall n\in N\exists k\in NQ\left(n\right)=k$$