| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1136 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) → 𝐾 ∈ HL) | 
| 2 |  | 1cvratex.b | . . . . 5
⊢ 𝐵 = (Base‘𝐾) | 
| 3 |  | 1cvratex.u | . . . . 5
⊢  1 =
(1.‘𝐾) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(oc‘𝐾) =
(oc‘𝐾) | 
| 5 |  | 1cvratex.c | . . . . 5
⊢ 𝐶 = ( ⋖ ‘𝐾) | 
| 6 |  | 1cvratex.a | . . . . 5
⊢ 𝐴 = (Atoms‘𝐾) | 
| 7 | 2, 3, 4, 5, 6 | 1cvrco 39475 | . . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑋𝐶 1 ↔ ((oc‘𝐾)‘𝑋) ∈ 𝐴)) | 
| 8 | 7 | biimp3a 1470 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) → ((oc‘𝐾)‘𝑋) ∈ 𝐴) | 
| 9 |  | eqid 2736 | . . . 4
⊢
(join‘𝐾) =
(join‘𝐾) | 
| 10 | 9, 5, 6 | 2dim 39473 | . . 3
⊢ ((𝐾 ∈ HL ∧
((oc‘𝐾)‘𝑋) ∈ 𝐴) → ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) | 
| 11 | 1, 8, 10 | syl2anc 584 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) → ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) | 
| 12 |  | simp11 1203 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → 𝐾 ∈ HL) | 
| 13 |  | hlop 39364 | . . . . . . . 8
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) | 
| 14 | 12, 13 | syl 17 | . . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → 𝐾 ∈ OP) | 
| 15 | 12 | hllatd 39366 | . . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → 𝐾 ∈ Lat) | 
| 16 |  | simp12 1204 | . . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → 𝑋 ∈ 𝐵) | 
| 17 | 2, 4 | opoccl 39196 | . . . . . . . . 9
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) | 
| 18 | 14, 16, 17 | syl2anc 584 | . . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘𝑋) ∈ 𝐵) | 
| 19 |  | simp2l 1199 | . . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → 𝑞 ∈ 𝐴) | 
| 20 | 2, 6 | atbase 39291 | . . . . . . . . 9
⊢ (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐵) | 
| 21 | 19, 20 | syl 17 | . . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → 𝑞 ∈ 𝐵) | 
| 22 | 2, 9 | latjcl 18485 | . . . . . . . 8
⊢ ((𝐾 ∈ Lat ∧
((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ 𝑞 ∈ 𝐵) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∈ 𝐵) | 
| 23 | 15, 18, 21, 22 | syl3anc 1372 | . . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∈ 𝐵) | 
| 24 | 2, 4 | opoccl 39196 | . . . . . . 7
⊢ ((𝐾 ∈ OP ∧
(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∈ 𝐵) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ∈ 𝐵) | 
| 25 | 14, 23, 24 | syl2anc 584 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ∈ 𝐵) | 
| 26 |  | simp2r 1200 | . . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → 𝑟 ∈ 𝐴) | 
| 27 | 2, 6 | atbase 39291 | . . . . . . . . . . . . 13
⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → 𝑟 ∈ 𝐵) | 
| 29 | 2, 9 | latjcl 18485 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ Lat ∧
(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟) ∈ 𝐵) | 
| 30 | 15, 23, 28, 29 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟) ∈ 𝐵) | 
| 31 | 2, 4 | opoccl 39196 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ OP ∧
((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟) ∈ 𝐵) → ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) ∈ 𝐵) | 
| 32 | 14, 30, 31 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) ∈ 𝐵) | 
| 33 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 34 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(0.‘𝐾) =
(0.‘𝐾) | 
| 35 | 2, 33, 34 | op0le 39188 | . . . . . . . . . 10
⊢ ((𝐾 ∈ OP ∧
((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) ∈ 𝐵) → (0.‘𝐾)(le‘𝐾)((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) | 
| 36 | 14, 32, 35 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (0.‘𝐾)(le‘𝐾)((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) | 
| 37 |  | simp3r 1202 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) | 
| 38 |  | 1cvratex.s | . . . . . . . . . . . 12
⊢  < =
(lt‘𝐾) | 
| 39 | 2, 38, 5 | cvrlt 39272 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧
(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∈ 𝐵 ∧ ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟) ∈ 𝐵) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) < ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) | 
| 40 | 12, 23, 30, 37, 39 | syl31anc 1374 | . . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) < ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) | 
| 41 | 2, 38, 4 | opltcon3b 39206 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ OP ∧
(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∈ 𝐵 ∧ ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟) ∈ 𝐵) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) < ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟) ↔ ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)))) | 
| 42 | 14, 23, 30, 41 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) < ((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟) ↔ ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)))) | 
| 43 | 40, 42 | mpbid 232 | . . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞))) | 
| 44 |  | hlpos 39368 | . . . . . . . . . . 11
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) | 
| 45 | 12, 44 | syl 17 | . . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → 𝐾 ∈ Poset) | 
| 46 | 2, 34 | op0cl 39186 | . . . . . . . . . . 11
⊢ (𝐾 ∈ OP →
(0.‘𝐾) ∈ 𝐵) | 
| 47 | 14, 46 | syl 17 | . . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (0.‘𝐾) ∈ 𝐵) | 
| 48 | 2, 33, 38 | plelttr 18390 | . . . . . . . . . 10
⊢ ((𝐾 ∈ Poset ∧
((0.‘𝐾) ∈ 𝐵 ∧ ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) ∈ 𝐵 ∧ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ∈ 𝐵)) → (((0.‘𝐾)(le‘𝐾)((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) ∧ ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞))) → (0.‘𝐾) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)))) | 
| 49 | 45, 47, 32, 25, 48 | syl13anc 1373 | . . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (((0.‘𝐾)(le‘𝐾)((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) ∧ ((oc‘𝐾)‘((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞))) → (0.‘𝐾) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)))) | 
| 50 | 36, 43, 49 | mp2and 699 | . . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (0.‘𝐾) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞))) | 
| 51 | 38 | pltne 18380 | . . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ (0.‘𝐾) ∈ 𝐵 ∧ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ∈ 𝐵) → ((0.‘𝐾) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) → (0.‘𝐾) ≠ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)))) | 
| 52 | 12, 47, 25, 51 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((0.‘𝐾) < ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) → (0.‘𝐾) ≠ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)))) | 
| 53 | 50, 52 | mpd 15 | . . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (0.‘𝐾) ≠ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞))) | 
| 54 | 53 | necomd 2995 | . . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ≠ (0.‘𝐾)) | 
| 55 | 2, 33, 34, 6 | atle 39439 | . . . . . 6
⊢ ((𝐾 ∈ HL ∧
((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ∈ 𝐵 ∧ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ≠ (0.‘𝐾)) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞))) | 
| 56 | 12, 25, 54, 55 | syl3anc 1372 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞))) | 
| 57 |  | simp3l 1201 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) | 
| 58 | 2, 38, 5 | cvrlt 39272 | . . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧
((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∈ 𝐵) ∧ ((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) → ((oc‘𝐾)‘𝑋) < (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) | 
| 59 | 12, 18, 23, 57, 58 | syl31anc 1374 | . . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘𝑋) < (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) | 
| 60 | 2, 38, 4 | opltcon3b 39206 | . . . . . . . . . . 11
⊢ ((𝐾 ∈ OP ∧
((oc‘𝐾)‘𝑋) ∈ 𝐵 ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∈ 𝐵) → (((oc‘𝐾)‘𝑋) < (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ↔ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) < ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)))) | 
| 61 | 14, 18, 23, 60 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (((oc‘𝐾)‘𝑋) < (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ↔ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) < ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)))) | 
| 62 | 59, 61 | mpbid 232 | . . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) < ((oc‘𝐾)‘((oc‘𝐾)‘𝑋))) | 
| 63 | 2, 4 | opococ 39197 | . . . . . . . . . 10
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)) = 𝑋) | 
| 64 | 14, 16, 63 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘((oc‘𝐾)‘𝑋)) = 𝑋) | 
| 65 | 62, 64 | breqtrd 5168 | . . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) < 𝑋) | 
| 66 | 65 | adantr 480 | . . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) ∧ 𝑝 ∈ 𝐴) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) < 𝑋) | 
| 67 |  | simpl11 1248 | . . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ HL) | 
| 68 | 67, 44 | syl 17 | . . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) ∧ 𝑝 ∈ 𝐴) → 𝐾 ∈ Poset) | 
| 69 | 2, 6 | atbase 39291 | . . . . . . . . 9
⊢ (𝑝 ∈ 𝐴 → 𝑝 ∈ 𝐵) | 
| 70 | 69 | adantl 481 | . . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) ∧ 𝑝 ∈ 𝐴) → 𝑝 ∈ 𝐵) | 
| 71 | 25 | adantr 480 | . . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) ∧ 𝑝 ∈ 𝐴) → ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ∈ 𝐵) | 
| 72 |  | simpl12 1249 | . . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) ∧ 𝑝 ∈ 𝐴) → 𝑋 ∈ 𝐵) | 
| 73 | 2, 33, 38 | plelttr 18390 | . . . . . . . 8
⊢ ((𝐾 ∈ Poset ∧ (𝑝 ∈ 𝐵 ∧ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → ((𝑝(le‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ∧ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) < 𝑋) → 𝑝 < 𝑋)) | 
| 74 | 68, 70, 71, 72, 73 | syl13anc 1373 | . . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) ∧ 𝑝 ∈ 𝐴) → ((𝑝(le‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) ∧ ((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) < 𝑋) → 𝑝 < 𝑋)) | 
| 75 | 66, 74 | mpan2d 694 | . . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) ∧ 𝑝 ∈ 𝐴) → (𝑝(le‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) → 𝑝 < 𝑋)) | 
| 76 | 75 | reximdva 3167 | . . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → (∃𝑝 ∈ 𝐴 𝑝(le‘𝐾)((oc‘𝐾)‘(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)) → ∃𝑝 ∈ 𝐴 𝑝 < 𝑋)) | 
| 77 | 56, 76 | mpd 15 | . . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) ∧ (𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟))) → ∃𝑝 ∈ 𝐴 𝑝 < 𝑋) | 
| 78 | 77 | 3exp 1119 | . . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) → ((𝑞 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → ((((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) → ∃𝑝 ∈ 𝐴 𝑝 < 𝑋))) | 
| 79 | 78 | rexlimdvv 3211 | . 2
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) → (∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (((oc‘𝐾)‘𝑋)𝐶(((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞) ∧ (((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)𝐶((((oc‘𝐾)‘𝑋)(join‘𝐾)𝑞)(join‘𝐾)𝑟)) → ∃𝑝 ∈ 𝐴 𝑝 < 𝑋)) | 
| 80 | 11, 79 | mpd 15 | 1
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) → ∃𝑝 ∈ 𝐴 𝑝 < 𝑋) |