Description: The extension of a permutation, fixing the additional element, is a bijection. (Contributed by AV, 7-Jan-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | symgext.s | |- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) ) |
|
symgext.e | |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) ) |
||
Assertion | symgextf1o | |- ( ( K e. N /\ Z e. S ) -> E : N -1-1-onto-> N ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | symgext.s | |- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) ) |
|
2 | symgext.e | |- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) ) |
|
3 | 1 2 | symgextf1 | |- ( ( K e. N /\ Z e. S ) -> E : N -1-1-> N ) |
4 | 1 2 | symgextfo | |- ( ( K e. N /\ Z e. S ) -> E : N -onto-> N ) |
5 | df-f1o | |- ( E : N -1-1-onto-> N <-> ( E : N -1-1-> N /\ E : N -onto-> N ) ) |
|
6 | 3 4 5 | sylanbrc | |- ( ( K e. N /\ Z e. S ) -> E : N -1-1-onto-> N ) |