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.d |
|- D = ( N \ { K } ) |
5 |
1 2
|
symgfixelq |
|- ( F e. Q -> ( F e. Q <-> ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) ) |
6 |
|
f1of1 |
|- ( F : N -1-1-onto-> N -> F : N -1-1-> N ) |
7 |
6
|
ad2antrl |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> F : N -1-1-> N ) |
8 |
|
difssd |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( N \ { K } ) C_ N ) |
9 |
|
f1ores |
|- ( ( F : N -1-1-> N /\ ( N \ { K } ) C_ N ) -> ( F |` ( N \ { K } ) ) : ( N \ { K } ) -1-1-onto-> ( F " ( N \ { K } ) ) ) |
10 |
7 8 9
|
syl2anc |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( F |` ( N \ { K } ) ) : ( N \ { K } ) -1-1-onto-> ( F " ( N \ { K } ) ) ) |
11 |
4
|
reseq2i |
|- ( F |` D ) = ( F |` ( N \ { K } ) ) |
12 |
11
|
a1i |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( F |` D ) = ( F |` ( N \ { K } ) ) ) |
13 |
4
|
a1i |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> D = ( N \ { K } ) ) |
14 |
|
f1ofo |
|- ( F : N -1-1-onto-> N -> F : N -onto-> N ) |
15 |
|
foima |
|- ( F : N -onto-> N -> ( F " N ) = N ) |
16 |
15
|
eqcomd |
|- ( F : N -onto-> N -> N = ( F " N ) ) |
17 |
14 16
|
syl |
|- ( F : N -1-1-onto-> N -> N = ( F " N ) ) |
18 |
17
|
ad2antrl |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> N = ( F " N ) ) |
19 |
|
sneq |
|- ( K = ( F ` K ) -> { K } = { ( F ` K ) } ) |
20 |
19
|
eqcoms |
|- ( ( F ` K ) = K -> { K } = { ( F ` K ) } ) |
21 |
20
|
ad2antll |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> { K } = { ( F ` K ) } ) |
22 |
|
f1ofn |
|- ( F : N -1-1-onto-> N -> F Fn N ) |
23 |
22
|
ad2antrl |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> F Fn N ) |
24 |
|
simpl |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> K e. N ) |
25 |
|
fnsnfv |
|- ( ( F Fn N /\ K e. N ) -> { ( F ` K ) } = ( F " { K } ) ) |
26 |
23 24 25
|
syl2anc |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> { ( F ` K ) } = ( F " { K } ) ) |
27 |
21 26
|
eqtrd |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> { K } = ( F " { K } ) ) |
28 |
18 27
|
difeq12d |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( N \ { K } ) = ( ( F " N ) \ ( F " { K } ) ) ) |
29 |
|
dff1o2 |
|- ( F : N -1-1-onto-> N <-> ( F Fn N /\ Fun `' F /\ ran F = N ) ) |
30 |
29
|
simp2bi |
|- ( F : N -1-1-onto-> N -> Fun `' F ) |
31 |
30
|
ad2antrl |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> Fun `' F ) |
32 |
|
imadif |
|- ( Fun `' F -> ( F " ( N \ { K } ) ) = ( ( F " N ) \ ( F " { K } ) ) ) |
33 |
31 32
|
syl |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( F " ( N \ { K } ) ) = ( ( F " N ) \ ( F " { K } ) ) ) |
34 |
28 13 33
|
3eqtr4d |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> D = ( F " ( N \ { K } ) ) ) |
35 |
12 13 34
|
f1oeq123d |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( ( F |` D ) : D -1-1-onto-> D <-> ( F |` ( N \ { K } ) ) : ( N \ { K } ) -1-1-onto-> ( F " ( N \ { K } ) ) ) ) |
36 |
10 35
|
mpbird |
|- ( ( K e. N /\ ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) ) -> ( F |` D ) : D -1-1-onto-> D ) |
37 |
36
|
ancoms |
|- ( ( ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) /\ K e. N ) -> ( F |` D ) : D -1-1-onto-> D ) |
38 |
1 2 3 4
|
symgfixels |
|- ( F e. Q -> ( ( F |` D ) e. S <-> ( F |` D ) : D -1-1-onto-> D ) ) |
39 |
37 38
|
syl5ibr |
|- ( F e. Q -> ( ( ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) /\ K e. N ) -> ( F |` D ) e. S ) ) |
40 |
39
|
expd |
|- ( F e. Q -> ( ( F : N -1-1-onto-> N /\ ( F ` K ) = K ) -> ( K e. N -> ( F |` D ) e. S ) ) ) |
41 |
5 40
|
sylbid |
|- ( F e. Q -> ( F e. Q -> ( K e. N -> ( F |` D ) e. S ) ) ) |
42 |
41
|
pm2.43i |
|- ( F e. Q -> ( K e. N -> ( F |` D ) e. S ) ) |
43 |
42
|
impcom |
|- ( ( K e. N /\ F e. Q ) -> ( F |` D ) e. S ) |