Metamath Proof Explorer


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 = ( Base ` ( SymGrp ` N ) )
Assertion symgmov1
|- ( Q e. P -> A. n e. N E. k e. N ( Q ` n ) = k )

Proof

Step Hyp Ref Expression
1 symgmov1.p
 |-  P = ( Base ` ( SymGrp ` N ) )
2 eqid
 |-  ( SymGrp ` N ) = ( SymGrp ` N )
3 2 1 symgfv
 |-  ( ( Q e. P /\ n e. N ) -> ( Q ` n ) e. N )
4 clel5
 |-  ( ( Q ` n ) e. N <-> E. k e. N ( Q ` n ) = k )
5 3 4 sylib
 |-  ( ( Q e. P /\ n e. N ) -> E. k e. N ( Q ` n ) = k )
6 5 ralrimiva
 |-  ( Q e. P -> A. n e. N E. k e. N ( Q ` n ) = k )