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 ˙ = K
1cvratlt.s < ˙ = < K
1cvratlt.u 1 ˙ = 1. K
1cvratlt.c C = K
1cvratlt.a A = Atoms K
Assertion 1cvratlt K HL P A X B X C 1 ˙ P ˙ X P < ˙ X

Proof

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