Step |
Hyp |
Ref |
Expression |
1 |
|
ldilset.b |
|- B = ( Base ` K ) |
2 |
|
ldilset.l |
|- .<_ = ( le ` K ) |
3 |
|
ldilset.h |
|- H = ( LHyp ` K ) |
4 |
|
ldilset.i |
|- I = ( LAut ` K ) |
5 |
|
ldilset.d |
|- D = ( ( LDil ` K ) ` W ) |
6 |
1 2 3 4
|
ldilfset |
|- ( K e. C -> ( LDil ` K ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) ) |
7 |
6
|
fveq1d |
|- ( K e. C -> ( ( LDil ` K ) ` W ) = ( ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) ` W ) ) |
8 |
|
breq2 |
|- ( w = W -> ( x .<_ w <-> x .<_ W ) ) |
9 |
8
|
imbi1d |
|- ( w = W -> ( ( x .<_ w -> ( f ` x ) = x ) <-> ( x .<_ W -> ( f ` x ) = x ) ) ) |
10 |
9
|
ralbidv |
|- ( w = W -> ( A. x e. B ( x .<_ w -> ( f ` x ) = x ) <-> A. x e. B ( x .<_ W -> ( f ` x ) = x ) ) ) |
11 |
10
|
rabbidv |
|- ( w = W -> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } ) |
12 |
|
eqid |
|- ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) |
13 |
4
|
fvexi |
|- I e. _V |
14 |
13
|
rabex |
|- { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } e. _V |
15 |
11 12 14
|
fvmpt |
|- ( W e. H -> ( ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) ` W ) = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } ) |
16 |
7 15
|
sylan9eq |
|- ( ( K e. C /\ W e. H ) -> ( ( LDil ` K ) ` W ) = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } ) |
17 |
5 16
|
syl5eq |
|- ( ( K e. C /\ W e. H ) -> D = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } ) |