This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
1cvratex.s ⊢ < = ( lt ‘ 𝐾 )
1cvratex.u ⊢ 1 = ( 1. ‘ 𝐾 )
1cvratex.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
1cvratex.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 1cvratex ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 𝐶 1 ) → ∃ 𝑝 ∈ 𝐴 𝑝 < 𝑋 )

Proof

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