| Step |
Hyp |
Ref |
Expression |
| 1 |
|
symgfixf.p |
|- P = ( Base ` ( SymGrp ` N ) ) |
| 2 |
|
symgfixf.q |
|- Q = { q e. P | ( q ` K ) = K } |
| 3 |
|
symgfixf.s |
|- S = ( Base ` ( SymGrp ` ( N \ { K } ) ) ) |
| 4 |
|
symgfixf.h |
|- H = ( q e. Q |-> ( q |` ( N \ { K } ) ) ) |
| 5 |
|
symgfixfo.e |
|- E = ( x e. N |-> if ( x = K , K , ( Z ` x ) ) ) |
| 6 |
3 5
|
symgextf1o |
|- ( ( K e. N /\ Z e. S ) -> E : N -1-1-onto-> N ) |
| 7 |
6
|
3adant1 |
|- ( ( N e. V /\ K e. N /\ Z e. S ) -> E : N -1-1-onto-> N ) |
| 8 |
|
iftrue |
|- ( x = K -> if ( x = K , K , ( Z ` x ) ) = K ) |
| 9 |
|
simp2 |
|- ( ( N e. V /\ K e. N /\ Z e. S ) -> K e. N ) |
| 10 |
5 8 9 9
|
fvmptd3 |
|- ( ( N e. V /\ K e. N /\ Z e. S ) -> ( E ` K ) = K ) |
| 11 |
|
mptexg |
|- ( N e. V -> ( x e. N |-> if ( x = K , K , ( Z ` x ) ) ) e. _V ) |
| 12 |
11
|
3ad2ant1 |
|- ( ( N e. V /\ K e. N /\ Z e. S ) -> ( x e. N |-> if ( x = K , K , ( Z ` x ) ) ) e. _V ) |
| 13 |
5 12
|
eqeltrid |
|- ( ( N e. V /\ K e. N /\ Z e. S ) -> E e. _V ) |
| 14 |
1 2
|
symgfixelq |
|- ( E e. _V -> ( E e. Q <-> ( E : N -1-1-onto-> N /\ ( E ` K ) = K ) ) ) |
| 15 |
13 14
|
syl |
|- ( ( N e. V /\ K e. N /\ Z e. S ) -> ( E e. Q <-> ( E : N -1-1-onto-> N /\ ( E ` K ) = K ) ) ) |
| 16 |
7 10 15
|
mpbir2and |
|- ( ( N e. V /\ K e. N /\ Z e. S ) -> E e. Q ) |