Metamath Proof Explorer

Theorem lhp2lt

Description: The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013)

Ref Expression
Hypotheses lhp2lt.l ⊢ ≤ = ( le ‘ 𝐾 )
lhp2lt.s ⊢ < = ( lt ‘ 𝐾 )
lhp2lt.j ⊢ ∨ = ( join ‘ 𝐾 )
lhp2lt.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lhp2lt.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhp2lt ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) < 𝑊 )

Proof

Step Hyp Ref Expression
1 lhp2lt.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lhp2lt.s ⊢ < = ( lt ‘ 𝐾 )
3 lhp2lt.j ⊢ ∨ = ( join ‘ 𝐾 )
4 lhp2lt.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 lhp2lt.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6 simp2r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝑃 ≤ 𝑊 )
7 simp3r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝑄 ≤ 𝑊 )
8 simp1l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝐾 ∈ HL )
9 8 hllatd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝐾 ∈ Lat )
10 simp2l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝑃 ∈ 𝐴 )
11 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12 11 4 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
13 10 12 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
14 simp3l ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝑄 ∈ 𝐴 )
15 11 4 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
16 14 15 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
17 simp1r ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝑊 ∈ 𝐻 )
18 11 5 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
19 17 18 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
20 11 1 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
21 9 13 16 19 20 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑃 ≤ 𝑊 ∧ 𝑄 ≤ 𝑊 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ) )
22 6 7 21 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 )
23 3 1 4 3dim2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
24 8 10 14 23 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
25 simp11l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → 𝐾 ∈ HL )
26 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
27 25 26 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → 𝐾 ∈ OP )
28 25 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → 𝐾 ∈ Lat )
29 simp12l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → 𝑃 ∈ 𝐴 )
30 simp13l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → 𝑄 ∈ 𝐴 )
31 11 3 4 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
32 25 29 30 31 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
33 simp2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → 𝑟 ∈ 𝐴 )
34 11 4 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) )
35 33 34 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
36 11 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
37 28 32 35 36 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
38 simp2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → 𝑠 ∈ 𝐴 )
39 11 4 atbase ⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ∈ ( Base ‘ 𝐾 ) )
40 38 39 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → 𝑠 ∈ ( Base ‘ 𝐾 ) )
41 11 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑠 ∈ ( Base ‘ 𝐾 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) ∈ ( Base ‘ 𝐾 ) )
42 28 37 40 41 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) ∈ ( Base ‘ 𝐾 ) )
43 eqid ⊢ ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
44 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
45 11 43 44 ncvr1 ⊢ ( ( 𝐾 ∈ OP ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) ∈ ( Base ‘ 𝐾 ) ) → ¬ ( 1. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) )
46 27 42 45 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → ¬ ( 1. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) )
47 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
48 simpl1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝐾 ∈ HL )
49 48 hllatd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝐾 ∈ Lat )
50 simpl2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝑃 ∈ 𝐴 )
51 simpl3l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝑄 ∈ 𝐴 )
52 48 50 51 31 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
53 simpr1l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝑟 ∈ 𝐴 )
54 53 34 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
55 49 52 54 36 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) )
56 48 26 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝐾 ∈ OP )
57 eqid ⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
58 11 47 57 op01dm ⊢ ( 𝐾 ∈ OP → ( ( Base ‘ 𝐾 ) ∈ dom ( lub ‘ 𝐾 ) ∧ ( Base ‘ 𝐾 ) ∈ dom ( glb ‘ 𝐾 ) ) )
59 58 simpld ⊢ ( 𝐾 ∈ OP → ( Base ‘ 𝐾 ) ∈ dom ( lub ‘ 𝐾 ) )
60 56 59 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( Base ‘ 𝐾 ) ∈ dom ( lub ‘ 𝐾 ) )
61 11 47 1 43 48 55 60 ple1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ≤ ( 1. ‘ 𝐾 ) )
62 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
63 48 62 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝐾 ∈ Poset )
64 11 43 op1cl ⊢ ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
65 56 64 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) )
66 simpr2l ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) )
67 11 1 3 44 4 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ 𝐴 ) → ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ 𝑄 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
68 48 52 53 67 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ 𝑄 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) )
69 66 68 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) )
70 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) = 𝑊 )
71 simpl1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝑊 ∈ 𝐻 )
72 43 44 5 lhp1cvr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
73 48 71 72 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝑊 ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
74 70 73 eqbrtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) )
75 11 1 44 cvrcmp ⊢ ( ( 𝐾 ∈ Poset ∧ ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 1. ‘ 𝐾 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ( ( 𝑃 ∨ 𝑄 ) ( ⋖ ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∧ ( 𝑃 ∨ 𝑄 ) ( ⋖ ‘ 𝐾 ) ( 1. ‘ 𝐾 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ≤ ( 1. ‘ 𝐾 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) = ( 1. ‘ 𝐾 ) ) )
76 63 55 65 52 69 74 75 syl132anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ≤ ( 1. ‘ 𝐾 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) = ( 1. ‘ 𝐾 ) ) )
77 61 76 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) = ( 1. ‘ 𝐾 ) )
78 simpr2r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) )
79 simpr1r ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → 𝑠 ∈ 𝐴 )
80 11 1 3 44 4 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑠 ∈ 𝐴 ) → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
81 48 55 79 80 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ↔ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
82 78 81 mpbid ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) )
83 77 82 eqbrtrrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ∧ ( 𝑃 ∨ 𝑄 ) = 𝑊 ) ) → ( 1. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) )
84 83 3exp2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → ( ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) → ( ( 𝑃 ∨ 𝑄 ) = 𝑊 → ( 1. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) ) ) ) )
85 84 3imp ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) = 𝑊 → ( 1. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) ) )
86 85 necon3bd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → ( ¬ ( 1. ‘ 𝐾 ) ( ⋖ ‘ 𝐾 ) ( ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ∨ 𝑠 ) → ( 𝑃 ∨ 𝑄 ) ≠ 𝑊 ) )
87 46 86 mpd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) ) → ( 𝑃 ∨ 𝑄 ) ≠ 𝑊 )
88 87 3exp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) → ( ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) → ( 𝑃 ∨ 𝑄 ) ≠ 𝑊 ) ) )
89 88 rexlimdvv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑟 ) ) → ( 𝑃 ∨ 𝑄 ) ≠ 𝑊 ) )
90 24 89 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) ≠ 𝑊 )
91 8 10 14 31 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
92 1 2 pltval ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑃 ∨ 𝑄 ) < 𝑊 ↔ ( ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑄 ) ≠ 𝑊 ) ) )
93 8 91 17 92 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( ( 𝑃 ∨ 𝑄 ) < 𝑊 ↔ ( ( 𝑃 ∨ 𝑄 ) ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑄 ) ≠ 𝑊 ) ) )
94 22 90 93 mpbir2and ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊 ) ) → ( 𝑃 ∨ 𝑄 ) < 𝑊 )