Step |
Hyp |
Ref |
Expression |
1 |
|
atlen0.b |
|- B = ( Base ` K ) |
2 |
|
atlen0.l |
|- .<_ = ( le ` K ) |
3 |
|
atlen0.z |
|- .0. = ( 0. ` K ) |
4 |
|
atlen0.a |
|- A = ( Atoms ` K ) |
5 |
|
simpl1 |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> K e. AtLat ) |
6 |
1 3
|
atl0cl |
|- ( K e. AtLat -> .0. e. B ) |
7 |
5 6
|
syl |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> .0. e. B ) |
8 |
|
simpl2 |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> X e. B ) |
9 |
5 7 8
|
3jca |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> ( K e. AtLat /\ .0. e. B /\ X e. B ) ) |
10 |
|
simpl3 |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> P e. A ) |
11 |
1 4
|
atbase |
|- ( P e. A -> P e. B ) |
12 |
10 11
|
syl |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> P e. B ) |
13 |
|
eqid |
|- ( |
14 |
3 13 4
|
atcvr0 |
|- ( ( K e. AtLat /\ P e. A ) -> .0. ( |
15 |
5 10 14
|
syl2anc |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> .0. ( |
16 |
|
eqid |
|- ( lt ` K ) = ( lt ` K ) |
17 |
1 16 13
|
cvrlt |
|- ( ( ( K e. AtLat /\ .0. e. B /\ P e. B ) /\ .0. ( .0. ( lt ` K ) P ) |
18 |
5 7 12 15 17
|
syl31anc |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> .0. ( lt ` K ) P ) |
19 |
|
simpr |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> P .<_ X ) |
20 |
|
atlpos |
|- ( K e. AtLat -> K e. Poset ) |
21 |
5 20
|
syl |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> K e. Poset ) |
22 |
1 2 16
|
pltletr |
|- ( ( K e. Poset /\ ( .0. e. B /\ P e. B /\ X e. B ) ) -> ( ( .0. ( lt ` K ) P /\ P .<_ X ) -> .0. ( lt ` K ) X ) ) |
23 |
21 7 12 8 22
|
syl13anc |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> ( ( .0. ( lt ` K ) P /\ P .<_ X ) -> .0. ( lt ` K ) X ) ) |
24 |
18 19 23
|
mp2and |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> .0. ( lt ` K ) X ) |
25 |
16
|
pltne |
|- ( ( K e. AtLat /\ .0. e. B /\ X e. B ) -> ( .0. ( lt ` K ) X -> .0. =/= X ) ) |
26 |
9 24 25
|
sylc |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> .0. =/= X ) |
27 |
26
|
necomd |
|- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> X =/= .0. ) |