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=BaseK
1cvratex.s ⊢<˙=<K
1cvratex.u ⊢1˙=1.⁡K
1cvratex.c ⊢C=⋖K
1cvratex.a ⊢A=Atoms⁡K
Assertion 1cvratex ⊢K∈HL∧X∈B∧XC1˙→∃p∈Ap<˙X

Proof

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