Metamath Proof Explorer


Theorem 1cvratex

Description: There exists an atom less than an element covered by 1. (Contributed by NM, 7-May-2012) (Revised by Mario Carneiro, 13-Jun-2014)

Ref Expression
Hypotheses 1cvratex.b B = Base K
1cvratex.s < ˙ = < K
1cvratex.u 1 ˙ = 1. K
1cvratex.c C = K
1cvratex.a A = Atoms K
Assertion 1cvratex K HL X B X C 1 ˙ p A p < ˙ X

Proof

Step Hyp Ref Expression
1 1cvratex.b B = Base K
2 1cvratex.s < ˙ = < K
3 1cvratex.u 1 ˙ = 1. K
4 1cvratex.c C = K
5 1cvratex.a A = Atoms K
6 simp1 K HL X B X C 1 ˙ K HL
7 eqid oc K = oc K
8 1 3 7 4 5 1cvrco K HL X B X C 1 ˙ oc K X A
9 8 biimp3a K HL X B X C 1 ˙ oc K X A
10 eqid join K = join K
11 10 4 5 2dim K HL oc K X A q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r
12 6 9 11 syl2anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r
13 simp11 K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r K HL
14 hlop K HL K OP
15 13 14 syl K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r K OP
16 13 hllatd K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r K Lat
17 simp12 K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r X B
18 1 7 opoccl K OP X B oc K X B
19 15 17 18 syl2anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K X B
20 simp2l K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r q A
21 1 5 atbase q A q B
22 20 21 syl K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r q B
23 1 10 latjcl K Lat oc K X B q B oc K X join K q B
24 16 19 22 23 syl3anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K X join K q B
25 1 7 opoccl K OP oc K X join K q B oc K oc K X join K q B
26 15 24 25 syl2anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K oc K X join K q B
27 simp2r K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r r A
28 1 5 atbase r A r B
29 27 28 syl K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r r B
30 1 10 latjcl K Lat oc K X join K q B r B oc K X join K q join K r B
31 16 24 29 30 syl3anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K X join K q join K r B
32 1 7 opoccl K OP oc K X join K q join K r B oc K oc K X join K q join K r B
33 15 31 32 syl2anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K oc K X join K q join K r B
34 eqid K = K
35 eqid 0. K = 0. K
36 1 34 35 op0le K OP oc K oc K X join K q join K r B 0. K K oc K oc K X join K q join K r
37 15 33 36 syl2anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r 0. K K oc K oc K X join K q join K r
38 simp3r K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K X join K q C oc K X join K q join K r
39 1 2 4 cvrlt K HL oc K X join K q B oc K X join K q join K r B oc K X join K q C oc K X join K q join K r oc K X join K q < ˙ oc K X join K q join K r
40 13 24 31 38 39 syl31anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K X join K q < ˙ oc K X join K q join K r
41 1 2 7 opltcon3b K OP oc K X join K q B oc K X join K q join K r B oc K X join K q < ˙ oc K X join K q join K r oc K oc K X join K q join K r < ˙ oc K oc K X join K q
42 15 24 31 41 syl3anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K X join K q < ˙ oc K X join K q join K r oc K oc K X join K q join K r < ˙ oc K oc K X join K q
43 40 42 mpbid K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K oc K X join K q join K r < ˙ oc K oc K X join K q
44 hlpos K HL K Poset
45 13 44 syl K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r K Poset
46 1 35 op0cl K OP 0. K B
47 15 46 syl K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r 0. K B
48 1 34 2 plelttr K Poset 0. K B oc K oc K X join K q join K r B oc K oc K X join K q B 0. K K oc K oc K X join K q join K r oc K oc K X join K q join K r < ˙ oc K oc K X join K q 0. K < ˙ oc K oc K X join K q
49 45 47 33 26 48 syl13anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r 0. K K oc K oc K X join K q join K r oc K oc K X join K q join K r < ˙ oc K oc K X join K q 0. K < ˙ oc K oc K X join K q
50 37 43 49 mp2and K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r 0. K < ˙ oc K oc K X join K q
51 2 pltne K HL 0. K B oc K oc K X join K q B 0. K < ˙ oc K oc K X join K q 0. K oc K oc K X join K q
52 13 47 26 51 syl3anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r 0. K < ˙ oc K oc K X join K q 0. K oc K oc K X join K q
53 50 52 mpd K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r 0. K oc K oc K X join K q
54 53 necomd K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K oc K X join K q 0. K
55 1 34 35 5 atle K HL oc K oc K X join K q B oc K oc K X join K q 0. K p A p K oc K oc K X join K q
56 13 26 54 55 syl3anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A p K oc K oc K X join K q
57 simp3l K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K X C oc K X join K q
58 1 2 4 cvrlt K HL oc K X B oc K X join K q B oc K X C oc K X join K q oc K X < ˙ oc K X join K q
59 13 19 24 57 58 syl31anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K X < ˙ oc K X join K q
60 1 2 7 opltcon3b K OP oc K X B oc K X join K q B oc K X < ˙ oc K X join K q oc K oc K X join K q < ˙ oc K oc K X
61 15 19 24 60 syl3anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K X < ˙ oc K X join K q oc K oc K X join K q < ˙ oc K oc K X
62 59 61 mpbid K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K oc K X join K q < ˙ oc K oc K X
63 1 7 opococ K OP X B oc K oc K X = X
64 15 17 63 syl2anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K oc K X = X
65 62 64 breqtrd K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r oc K oc K X join K q < ˙ X
66 65 adantr K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A oc K oc K X join K q < ˙ X
67 simpl11 K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A K HL
68 67 44 syl K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A K Poset
69 1 5 atbase p A p B
70 69 adantl K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A p B
71 26 adantr K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A oc K oc K X join K q B
72 simpl12 K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A X B
73 1 34 2 plelttr K Poset p B oc K oc K X join K q B X B p K oc K oc K X join K q oc K oc K X join K q < ˙ X p < ˙ X
74 68 70 71 72 73 syl13anc K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A p K oc K oc K X join K q oc K oc K X join K q < ˙ X p < ˙ X
75 66 74 mpan2d K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A p K oc K oc K X join K q p < ˙ X
76 75 reximdva K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A p K oc K oc K X join K q p A p < ˙ X
77 56 76 mpd K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A p < ˙ X
78 77 3exp K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A p < ˙ X
79 78 rexlimdvv K HL X B X C 1 ˙ q A r A oc K X C oc K X join K q oc K X join K q C oc K X join K q join K r p A p < ˙ X
80 12 79 mpd K HL X B X C 1 ˙ p A p < ˙ X