Step |
Hyp |
Ref |
Expression |
1 |
|
dicval.l |
|- .<_ = ( le ` K ) |
2 |
|
dicval.a |
|- A = ( Atoms ` K ) |
3 |
|
dicval.h |
|- H = ( LHyp ` K ) |
4 |
|
dicval.p |
|- P = ( ( oc ` K ) ` W ) |
5 |
|
dicval.t |
|- T = ( ( LTrn ` K ) ` W ) |
6 |
|
dicval.e |
|- E = ( ( TEndo ` K ) ` W ) |
7 |
|
dicval.i |
|- I = ( ( DIsoC ` K ) ` W ) |
8 |
|
dicval2.g |
|- G = ( iota_ g e. T ( g ` P ) = Q ) |
9 |
1 2 3 4 5 6 7
|
dicval |
|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } ) |
10 |
8
|
fveq2i |
|- ( s ` G ) = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) |
11 |
10
|
eqeq2i |
|- ( f = ( s ` G ) <-> f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) ) |
12 |
11
|
anbi1i |
|- ( ( f = ( s ` G ) /\ s e. E ) <-> ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) ) |
13 |
12
|
opabbii |
|- { <. f , s >. | ( f = ( s ` G ) /\ s e. E ) } = { <. f , s >. | ( f = ( s ` ( iota_ g e. T ( g ` P ) = Q ) ) /\ s e. E ) } |
14 |
9 13
|
eqtr4di |
|- ( ( ( K e. V /\ W e. H ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( I ` Q ) = { <. f , s >. | ( f = ( s ` G ) /\ s e. E ) } ) |