Step |
Hyp |
Ref |
Expression |
1 |
|
leatom.b |
|- B = ( Base ` K ) |
2 |
|
leatom.l |
|- .<_ = ( le ` K ) |
3 |
|
leatom.z |
|- .0. = ( 0. ` K ) |
4 |
|
leatom.a |
|- A = ( Atoms ` K ) |
5 |
1 2 3 4
|
leatb |
|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P <-> ( X = P \/ X = .0. ) ) ) |
6 |
|
orcom |
|- ( ( X = P \/ X = .0. ) <-> ( X = .0. \/ X = P ) ) |
7 |
|
neor |
|- ( ( X = .0. \/ X = P ) <-> ( X =/= .0. -> X = P ) ) |
8 |
6 7
|
bitri |
|- ( ( X = P \/ X = .0. ) <-> ( X =/= .0. -> X = P ) ) |
9 |
5 8
|
bitrdi |
|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P <-> ( X =/= .0. -> X = P ) ) ) |
10 |
9
|
biimpd |
|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P -> ( X =/= .0. -> X = P ) ) ) |
11 |
10
|
com23 |
|- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X =/= .0. -> ( X .<_ P -> X = P ) ) ) |
12 |
11
|
imp32 |
|- ( ( ( K e. OP /\ X e. B /\ P e. A ) /\ ( X =/= .0. /\ X .<_ P ) ) -> X = P ) |