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

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	symgbasf1o	$$⊢Q\in P\to Q:N\underset{1-1\; onto}{⟶}N$$
4		f1ofo	$$⊢Q:N\underset{1-1\; onto}{⟶}N\to Q:N\underset{onto}{⟶}N$$
5		foelcdmi	$$⊢\left(Q:N\underset{onto}{⟶}N\wedge n\in N\right)\to \exists k\in NQ\left(k\right)=n$$
6	5	ralrimiva	$$⊢Q:N\underset{onto}{⟶}N\to \forall n\in N\exists k\in NQ\left(k\right)=n$$
7	3 4 6	3syl	$$⊢Q\in P\to \forall n\in N\exists k\in NQ\left(k\right)=n$$