Step |
Hyp |
Ref |
Expression |
1 |
|
dicvalrel.h |
|- H = ( LHyp ` K ) |
2 |
|
dicvalrel.i |
|- I = ( ( DIsoC ` K ) ` W ) |
3 |
|
relopabv |
|- Rel { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = X ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } |
4 |
|
eqid |
|- ( le ` K ) = ( le ` K ) |
5 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
6 |
4 5 1 2
|
dicdmN |
|- ( ( K e. V /\ W e. H ) -> dom I = { p e. ( Atoms ` K ) | -. p ( le ` K ) W } ) |
7 |
6
|
eleq2d |
|- ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> X e. { p e. ( Atoms ` K ) | -. p ( le ` K ) W } ) ) |
8 |
|
breq1 |
|- ( p = X -> ( p ( le ` K ) W <-> X ( le ` K ) W ) ) |
9 |
8
|
notbid |
|- ( p = X -> ( -. p ( le ` K ) W <-> -. X ( le ` K ) W ) ) |
10 |
9
|
elrab |
|- ( X e. { p e. ( Atoms ` K ) | -. p ( le ` K ) W } <-> ( X e. ( Atoms ` K ) /\ -. X ( le ` K ) W ) ) |
11 |
7 10
|
bitrdi |
|- ( ( K e. V /\ W e. H ) -> ( X e. dom I <-> ( X e. ( Atoms ` K ) /\ -. X ( le ` K ) W ) ) ) |
12 |
11
|
biimpa |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> ( X e. ( Atoms ` K ) /\ -. X ( le ` K ) W ) ) |
13 |
|
eqid |
|- ( ( oc ` K ) ` W ) = ( ( oc ` K ) ` W ) |
14 |
|
eqid |
|- ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W ) |
15 |
|
eqid |
|- ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W ) |
16 |
4 5 1 13 14 15 2
|
dicval |
|- ( ( ( K e. V /\ W e. H ) /\ ( X e. ( Atoms ` K ) /\ -. X ( le ` K ) W ) ) -> ( I ` X ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = X ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) |
17 |
12 16
|
syldan |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> ( I ` X ) = { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = X ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) |
18 |
17
|
releqd |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> ( Rel ( I ` X ) <-> Rel { <. f , s >. | ( f = ( s ` ( iota_ g e. ( ( LTrn ` K ) ` W ) ( g ` ( ( oc ` K ) ` W ) ) = X ) ) /\ s e. ( ( TEndo ` K ) ` W ) ) } ) ) |
19 |
3 18
|
mpbiri |
|- ( ( ( K e. V /\ W e. H ) /\ X e. dom I ) -> Rel ( I ` X ) ) |
20 |
19
|
ex |
|- ( ( K e. V /\ W e. H ) -> ( X e. dom I -> Rel ( I ` X ) ) ) |
21 |
|
rel0 |
|- Rel (/) |
22 |
|
ndmfv |
|- ( -. X e. dom I -> ( I ` X ) = (/) ) |
23 |
22
|
releqd |
|- ( -. X e. dom I -> ( Rel ( I ` X ) <-> Rel (/) ) ) |
24 |
21 23
|
mpbiri |
|- ( -. X e. dom I -> Rel ( I ` X ) ) |
25 |
20 24
|
pm2.61d1 |
|- ( ( K e. V /\ W e. H ) -> Rel ( I ` X ) ) |