Metamath Proof Explorer

Theorem atnlt

Description: Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012)

Ref Expression
Hypotheses atnlt.s 
|- .< = ( lt ` K )
atnlt.a 
|- A = ( Atoms ` K )
Assertion atnlt 
|- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> -. P .< Q )

Proof

Step Hyp Ref Expression
1 atnlt.s 
 |-  .< = ( lt ` K )
2 atnlt.a 
 |-  A = ( Atoms ` K )
3 1 pltirr 
 |-  ( ( K e. AtLat /\ P e. A ) -> -. P .< P )
4 3 3adant3 
 |-  ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> -. P .< P )
5 breq2 
 |-  ( P = Q -> ( P .< P <-> P .< Q ) )
6 5 notbid 
 |-  ( P = Q -> ( -. P .< P <-> -. P .< Q ) )
7 4 6 syl5ibcom 
 |-  ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P = Q -> -. P .< Q ) )
8 eqid 
 |-  ( le ` K ) = ( le ` K )
9 8 1 pltle 
 |-  ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P .< Q -> P ( le ` K ) Q ) )
10 8 2 atcmp 
 |-  ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P ( le ` K ) Q <-> P = Q ) )
11 9 10 sylibd 
 |-  ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P .< Q -> P = Q ) )
12 11 necon3ad 
 |-  ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P =/= Q -> -. P .< Q ) )
13 7 12 pm2.61dne 
 |-  ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> -. P .< Q )