Metamath Proof Explorer

Theorem ncvr1

Description: No element covers the lattice unity. (Contributed by NM, 8-Jul-2013)

Ref Expression
Hypotheses ncvr1.b 
|- B = ( Base ` K )
ncvr1.u 
|- .1. = ( 1. ` K )
ncvr1.c 
|- C = (
Assertion ncvr1 
|- ( ( K e. OP /\ X e. B ) -> -. .1. C X )

Proof

Step Hyp Ref Expression
1 ncvr1.b 
 |-  B = ( Base ` K )
2 ncvr1.u 
 |-  .1. = ( 1. ` K )
3 ncvr1.c 
 |-  C = (
4 eqid 
 |-  ( le ` K ) = ( le ` K )
5 1 4 2 ople1 
 |-  ( ( K e. OP /\ X e. B ) -> X ( le ` K ) .1. )
6 opposet 
 |-  ( K e. OP -> K e. Poset )
7 6 ad2antrr 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. ( lt ` K ) X ) -> K e. Poset )
8 1 2 op1cl 
 |-  ( K e. OP -> .1. e. B )
9 8 ad2antrr 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. ( lt ` K ) X ) -> .1. e. B )
10 simplr 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. ( lt ` K ) X ) -> X e. B )
11 simpr 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. ( lt ` K ) X ) -> .1. ( lt ` K ) X )
12 eqid 
 |-  ( lt ` K ) = ( lt ` K )
13 1 4 12 pltnle 
 |-  ( ( ( K e. Poset /\ .1. e. B /\ X e. B ) /\ .1. ( lt ` K ) X ) -> -. X ( le ` K ) .1. )
14 7 9 10 11 13 syl31anc 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. ( lt ` K ) X ) -> -. X ( le ` K ) .1. )
15 14 ex 
 |-  ( ( K e. OP /\ X e. B ) -> ( .1. ( lt ` K ) X -> -. X ( le ` K ) .1. ) )
16 5 15 mt2d 
 |-  ( ( K e. OP /\ X e. B ) -> -. .1. ( lt ` K ) X )
17 simpll 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. C X ) -> K e. OP )
18 8 ad2antrr 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. C X ) -> .1. e. B )
19 simplr 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. C X ) -> X e. B )
20 simpr 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. C X ) -> .1. C X )
21 1 12 3 cvrlt 
 |-  ( ( ( K e. OP /\ .1. e. B /\ X e. B ) /\ .1. C X ) -> .1. ( lt ` K ) X )
22 17 18 19 20 21 syl31anc 
 |-  ( ( ( K e. OP /\ X e. B ) /\ .1. C X ) -> .1. ( lt ` K ) X )
23 16 22 mtand 
 |-  ( ( K e. OP /\ X e. B ) -> -. .1. C X )