Step |
Hyp |
Ref |
Expression |
1 |
|
pautset.s |
|- S = ( PSubSp ` K ) |
2 |
|
pautset.m |
|- M = ( PAut ` K ) |
3 |
1 2
|
pautsetN |
|- ( 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 ) ) ) } ) |
4 |
3
|
eleq2d |
|- ( K e. B -> ( F e. M <-> F e. { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } ) ) |
5 |
|
f1of |
|- ( F : S -1-1-onto-> S -> F : S --> S ) |
6 |
1
|
fvexi |
|- S e. _V |
7 |
|
fex |
|- ( ( F : S --> S /\ S e. _V ) -> F e. _V ) |
8 |
5 6 7
|
sylancl |
|- ( F : S -1-1-onto-> S -> F e. _V ) |
9 |
8
|
adantr |
|- ( ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) -> F e. _V ) |
10 |
|
f1oeq1 |
|- ( f = F -> ( f : S -1-1-onto-> S <-> F : S -1-1-onto-> S ) ) |
11 |
|
fveq1 |
|- ( f = F -> ( f ` x ) = ( F ` x ) ) |
12 |
|
fveq1 |
|- ( f = F -> ( f ` y ) = ( F ` y ) ) |
13 |
11 12
|
sseq12d |
|- ( f = F -> ( ( f ` x ) C_ ( f ` y ) <-> ( F ` x ) C_ ( F ` y ) ) ) |
14 |
13
|
bibi2d |
|- ( f = F -> ( ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) <-> ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) |
15 |
14
|
2ralbidv |
|- ( f = F -> ( A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) <-> A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) |
16 |
10 15
|
anbi12d |
|- ( f = F -> ( ( 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 /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) ) |
17 |
9 16
|
elab3 |
|- ( F e. { f | ( 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 /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) |
18 |
4 17
|
bitrdi |
|- ( K e. B -> ( F e. M <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) ) |