Step |
Hyp |
Ref |
Expression |
1 |
|
cvlexch3.b |
|- B = ( Base ` K ) |
2 |
|
cvlexch3.l |
|- .<_ = ( le ` K ) |
3 |
|
cvlexch3.j |
|- .\/ = ( join ` K ) |
4 |
|
cvlexch3.m |
|- ./\ = ( meet ` K ) |
5 |
|
cvlexch3.z |
|- .0. = ( 0. ` K ) |
6 |
|
cvlexch3.a |
|- A = ( Atoms ` K ) |
7 |
|
cvlatl |
|- ( K e. CvLat -> K e. AtLat ) |
8 |
7
|
adantr |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> K e. AtLat ) |
9 |
|
simpr1 |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> P e. A ) |
10 |
|
simpr3 |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> X e. B ) |
11 |
1 2 4 5 6
|
atnle |
|- ( ( K e. AtLat /\ P e. A /\ X e. B ) -> ( -. P .<_ X <-> ( P ./\ X ) = .0. ) ) |
12 |
8 9 10 11
|
syl3anc |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( -. P .<_ X <-> ( P ./\ X ) = .0. ) ) |
13 |
1 2 3 6
|
cvlexch1 |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) ) |
14 |
13
|
3expia |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( -. P .<_ X -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) ) ) |
15 |
12 14
|
sylbird |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) ) -> ( ( P ./\ X ) = .0. -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) ) ) |
16 |
15
|
3impia |
|- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P ./\ X ) = .0. ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) ) |