Metamath Proof Explorer

Theorem 1cvratlt

Description: An atom less than or equal to an element covered by 1 is less than the element. (Contributed by NM, 7-May-2012)

Ref Expression
Hypotheses 1cvratlt.b 
|- B = ( Base ` K )
1cvratlt.l 
|- .<_ = ( le ` K )
1cvratlt.s 
|- .< = ( lt ` K )
1cvratlt.u 
|- .1. = ( 1. ` K )
1cvratlt.c 
|- C = (
1cvratlt.a 
|- A = ( Atoms ` K )
Assertion 1cvratlt 
|- ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) -> P .< X )

Proof

Step Hyp Ref Expression
1 1cvratlt.b 
 |-  B = ( Base ` K )
2 1cvratlt.l 
 |-  .<_ = ( le ` K )
3 1cvratlt.s 
 |-  .< = ( lt ` K )
4 1cvratlt.u 
 |-  .1. = ( 1. ` K )
5 1cvratlt.c 
 |-  C = (
6 1cvratlt.a 
 |-  A = ( Atoms ` K )
7 simpl1 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) -> K e. HL )
8 simpl3 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) -> X e. B )
9 simprl 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) -> X C .1. )
10 1 3 4 5 6 1cvratex 
 |-  ( ( K e. HL /\ X e. B /\ X C .1. ) -> E. q e. A q .< X )
11 7 8 9 10 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) -> E. q e. A q .< X )
12 simp1l1 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) /\ q e. A /\ q .< X ) -> K e. HL )
13 simp1l2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) /\ q e. A /\ q .< X ) -> P e. A )
14 simp2 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) /\ q e. A /\ q .< X ) -> q e. A )
15 simp1l3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) /\ q e. A /\ q .< X ) -> X e. B )
16 simp1rr 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) /\ q e. A /\ q .< X ) -> P .<_ X )
17 simp3 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) /\ q e. A /\ q .< X ) -> q .< X )
18 1 2 3 6 atlelt 
 |-  ( ( K e. HL /\ ( P e. A /\ q e. A /\ X e. B ) /\ ( P .<_ X /\ q .< X ) ) -> P .< X )
19 12 13 14 15 16 17 18 syl132anc 
 |-  ( ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) /\ q e. A /\ q .< X ) -> P .< X )
20 19 rexlimdv3a 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) -> ( E. q e. A q .< X -> P .< X ) )
21 11 20 mpd 
 |-  ( ( ( K e. HL /\ P e. A /\ X e. B ) /\ ( X C .1. /\ P .<_ X ) ) -> P .< X )