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