Step |
Hyp |
Ref |
Expression |
1 |
|
pautset.s |
|- S = ( PSubSp ` K ) |
2 |
|
pautset.m |
|- M = ( PAut ` K ) |
3 |
|
elex |
|- ( K e. B -> K e. _V ) |
4 |
|
fveq2 |
|- ( k = K -> ( PSubSp ` k ) = ( PSubSp ` K ) ) |
5 |
4 1
|
eqtr4di |
|- ( k = K -> ( PSubSp ` k ) = S ) |
6 |
5
|
f1oeq2d |
|- ( k = K -> ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) <-> f : S -1-1-onto-> ( PSubSp ` k ) ) ) |
7 |
|
f1oeq3 |
|- ( ( PSubSp ` k ) = S -> ( f : S -1-1-onto-> ( PSubSp ` k ) <-> f : S -1-1-onto-> S ) ) |
8 |
5 7
|
syl |
|- ( k = K -> ( f : S -1-1-onto-> ( PSubSp ` k ) <-> f : S -1-1-onto-> S ) ) |
9 |
6 8
|
bitrd |
|- ( k = K -> ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) <-> f : S -1-1-onto-> S ) ) |
10 |
5
|
raleqdv |
|- ( k = K -> ( A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) <-> A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) ) |
11 |
5 10
|
raleqbidv |
|- ( k = K -> ( A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) <-> A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) ) |
12 |
9 11
|
anbi12d |
|- ( k = K -> ( ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) /\ A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) <-> ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) ) ) |
13 |
12
|
abbidv |
|- ( k = K -> { f | ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) /\ A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } = { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } ) |
14 |
|
df-pautN |
|- PAut = ( k e. _V |-> { f | ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) /\ A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } ) |
15 |
1
|
fvexi |
|- S e. _V |
16 |
15 15
|
mapval |
|- ( S ^m S ) = { f | f : S --> S } |
17 |
|
ovex |
|- ( S ^m S ) e. _V |
18 |
16 17
|
eqeltrri |
|- { f | f : S --> S } e. _V |
19 |
|
f1of |
|- ( f : S -1-1-onto-> S -> f : S --> S ) |
20 |
19
|
ss2abi |
|- { f | f : S -1-1-onto-> S } C_ { f | f : S --> S } |
21 |
18 20
|
ssexi |
|- { f | f : S -1-1-onto-> S } e. _V |
22 |
|
simpl |
|- ( ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) -> f : S -1-1-onto-> S ) |
23 |
22
|
ss2abi |
|- { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } C_ { f | f : S -1-1-onto-> S } |
24 |
21 23
|
ssexi |
|- { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } e. _V |
25 |
13 14 24
|
fvmpt |
|- ( K e. _V -> ( PAut ` K ) = { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } ) |
26 |
2 25
|
syl5eq |
|- ( K e. _V -> M = { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } ) |
27 |
3 26
|
syl |
|- ( K e. B -> M = { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } ) |