Step |
Hyp |
Ref |
Expression |
1 |
|
ltrnset.l |
|- .<_ = ( le ` K ) |
2 |
|
ltrnset.j |
|- .\/ = ( join ` K ) |
3 |
|
ltrnset.m |
|- ./\ = ( meet ` K ) |
4 |
|
ltrnset.a |
|- A = ( Atoms ` K ) |
5 |
|
ltrnset.h |
|- H = ( LHyp ` K ) |
6 |
|
ltrnset.d |
|- D = ( ( LDil ` K ) ` W ) |
7 |
|
ltrnset.t |
|- T = ( ( LTrn ` K ) ` W ) |
8 |
1 2 3 4 5
|
ltrnfset |
|- ( K e. B -> ( LTrn ` K ) = ( w e. H |-> { f e. ( ( LDil ` K ) ` w ) | A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) } ) ) |
9 |
8
|
fveq1d |
|- ( K e. B -> ( ( LTrn ` K ) ` W ) = ( ( w e. H |-> { f e. ( ( LDil ` K ) ` w ) | A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) } ) ` W ) ) |
10 |
7 9
|
syl5eq |
|- ( K e. B -> T = ( ( w e. H |-> { f e. ( ( LDil ` K ) ` w ) | A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) } ) ` W ) ) |
11 |
|
fveq2 |
|- ( w = W -> ( ( LDil ` K ) ` w ) = ( ( LDil ` K ) ` W ) ) |
12 |
11 6
|
eqtr4di |
|- ( w = W -> ( ( LDil ` K ) ` w ) = D ) |
13 |
|
breq2 |
|- ( w = W -> ( p .<_ w <-> p .<_ W ) ) |
14 |
13
|
notbid |
|- ( w = W -> ( -. p .<_ w <-> -. p .<_ W ) ) |
15 |
|
breq2 |
|- ( w = W -> ( q .<_ w <-> q .<_ W ) ) |
16 |
15
|
notbid |
|- ( w = W -> ( -. q .<_ w <-> -. q .<_ W ) ) |
17 |
14 16
|
anbi12d |
|- ( w = W -> ( ( -. p .<_ w /\ -. q .<_ w ) <-> ( -. p .<_ W /\ -. q .<_ W ) ) ) |
18 |
|
oveq2 |
|- ( w = W -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( p .\/ ( f ` p ) ) ./\ W ) ) |
19 |
|
oveq2 |
|- ( w = W -> ( ( q .\/ ( f ` q ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) |
20 |
18 19
|
eqeq12d |
|- ( w = W -> ( ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) <-> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) ) |
21 |
17 20
|
imbi12d |
|- ( w = W -> ( ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) <-> ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) ) ) |
22 |
21
|
2ralbidv |
|- ( w = W -> ( A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) <-> A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) ) ) |
23 |
12 22
|
rabeqbidv |
|- ( w = W -> { f e. ( ( LDil ` K ) ` w ) | A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) } = { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } ) |
24 |
|
eqid |
|- ( w e. H |-> { f e. ( ( LDil ` K ) ` w ) | A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) } ) = ( w e. H |-> { f e. ( ( LDil ` K ) ` w ) | A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) } ) |
25 |
6
|
fvexi |
|- D e. _V |
26 |
25
|
rabex |
|- { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } e. _V |
27 |
23 24 26
|
fvmpt |
|- ( W e. H -> ( ( w e. H |-> { f e. ( ( LDil ` K ) ` w ) | A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) } ) ` W ) = { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } ) |
28 |
10 27
|
sylan9eq |
|- ( ( K e. B /\ W e. H ) -> T = { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } ) |