Step |
Hyp |
Ref |
Expression |
1 |
|
meetle.b |
|- B = ( Base ` K ) |
2 |
|
meetle.l |
|- .<_ = ( le ` K ) |
3 |
|
meetle.m |
|- ./\ = ( meet ` K ) |
4 |
|
meetle.k |
|- ( ph -> K e. Poset ) |
5 |
|
meetle.x |
|- ( ph -> X e. B ) |
6 |
|
meetle.y |
|- ( ph -> Y e. B ) |
7 |
|
meetle.z |
|- ( ph -> Z e. B ) |
8 |
|
meetle.e |
|- ( ph -> <. X , Y >. e. dom ./\ ) |
9 |
|
breq1 |
|- ( z = Z -> ( z .<_ X <-> Z .<_ X ) ) |
10 |
|
breq1 |
|- ( z = Z -> ( z .<_ Y <-> Z .<_ Y ) ) |
11 |
9 10
|
anbi12d |
|- ( z = Z -> ( ( z .<_ X /\ z .<_ Y ) <-> ( Z .<_ X /\ Z .<_ Y ) ) ) |
12 |
|
breq1 |
|- ( z = Z -> ( z .<_ ( X ./\ Y ) <-> Z .<_ ( X ./\ Y ) ) ) |
13 |
11 12
|
imbi12d |
|- ( z = Z -> ( ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) <-> ( ( Z .<_ X /\ Z .<_ Y ) -> Z .<_ ( X ./\ Y ) ) ) ) |
14 |
1 2 3 4 5 6 8
|
meetlem |
|- ( ph -> ( ( ( X ./\ Y ) .<_ X /\ ( X ./\ Y ) .<_ Y ) /\ A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) ) ) |
15 |
14
|
simprd |
|- ( ph -> A. z e. B ( ( z .<_ X /\ z .<_ Y ) -> z .<_ ( X ./\ Y ) ) ) |
16 |
13 15 7
|
rspcdva |
|- ( ph -> ( ( Z .<_ X /\ Z .<_ Y ) -> Z .<_ ( X ./\ Y ) ) ) |
17 |
1 2 3 4 5 6 8
|
lemeet1 |
|- ( ph -> ( X ./\ Y ) .<_ X ) |
18 |
1 3 4 5 6 8
|
meetcl |
|- ( ph -> ( X ./\ Y ) e. B ) |
19 |
1 2
|
postr |
|- ( ( K e. Poset /\ ( Z e. B /\ ( X ./\ Y ) e. B /\ X e. B ) ) -> ( ( Z .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ X ) -> Z .<_ X ) ) |
20 |
4 7 18 5 19
|
syl13anc |
|- ( ph -> ( ( Z .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ X ) -> Z .<_ X ) ) |
21 |
17 20
|
mpan2d |
|- ( ph -> ( Z .<_ ( X ./\ Y ) -> Z .<_ X ) ) |
22 |
1 2 3 4 5 6 8
|
lemeet2 |
|- ( ph -> ( X ./\ Y ) .<_ Y ) |
23 |
1 2
|
postr |
|- ( ( K e. Poset /\ ( Z e. B /\ ( X ./\ Y ) e. B /\ Y e. B ) ) -> ( ( Z .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ Y ) -> Z .<_ Y ) ) |
24 |
4 7 18 6 23
|
syl13anc |
|- ( ph -> ( ( Z .<_ ( X ./\ Y ) /\ ( X ./\ Y ) .<_ Y ) -> Z .<_ Y ) ) |
25 |
22 24
|
mpan2d |
|- ( ph -> ( Z .<_ ( X ./\ Y ) -> Z .<_ Y ) ) |
26 |
21 25
|
jcad |
|- ( ph -> ( Z .<_ ( X ./\ Y ) -> ( Z .<_ X /\ Z .<_ Y ) ) ) |
27 |
16 26
|
impbid |
|- ( ph -> ( ( Z .<_ X /\ Z .<_ Y ) <-> Z .<_ ( X ./\ Y ) ) ) |