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 ) |
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 ) |