Metamath Proof Explorer

Theorem cvrat4

Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in PtakPulmannova p. 68. Also Lemma 9.2(delta) in MaedaMaeda p. 41. ( atcvat4i analog.) (Contributed by NM, 30-Nov-2011)

Ref Expression
Hypotheses cvrat4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrat4.l ⊢ ≤ = ( le ‘ 𝐾 )
cvrat4.j ⊢ ∨ = ( join ‘ 𝐾 )
cvrat4.z ⊢ 0 = ( 0. ‘ 𝐾 )
cvrat4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvrat4 ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) )

Proof

Step Hyp Ref Expression
1 cvrat4.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrat4.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvrat4.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvrat4.z ⊢ 0 = ( 0. ‘ 𝐾 )
5 cvrat4.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
7 6 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ AtLat )
8 simpr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
9 1 2 4 5 atlex ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃ 𝑟 ∈ 𝐴 𝑟 ≤ 𝑋 )
10 9 3exp ⊢ ( 𝐾 ∈ AtLat → ( 𝑋 ∈ 𝐵 → ( 𝑋 ≠ 0 → ∃ 𝑟 ∈ 𝐴 𝑟 ≤ 𝑋 ) ) )
11 7 8 10 sylc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ≠ 0 → ∃ 𝑟 ∈ 𝐴 𝑟 ≤ 𝑋 ) )
12 11 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑋 ≠ 0 → ∃ 𝑟 ∈ 𝐴 𝑟 ≤ 𝑋 ) )
13 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ HL )
14 simplr3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
15 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑟 ∈ 𝐴 )
16 2 3 5 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑄 ∨ 𝑟 ) )
17 13 14 15 16 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑄 ≤ ( 𝑄 ∨ 𝑟 ) )
18 breq1 ⊢ ( 𝑃 = 𝑄 → ( 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ↔ 𝑄 ≤ ( 𝑄 ∨ 𝑟 ) ) )
19 17 18 imbitrrid ⊢ ( 𝑃 = 𝑄 → ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) )
20 19 expd ⊢ ( 𝑃 = 𝑄 → ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑟 ∈ 𝐴 → 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) )
21 20 impcom ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑟 ∈ 𝐴 → 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) )
22 21 anim2d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ( ( 𝑟 ≤ 𝑋 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) )
23 22 expcomd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑟 ∈ 𝐴 → ( 𝑟 ≤ 𝑋 → ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) )
24 23 reximdvai ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ( ∃ 𝑟 ∈ 𝐴 𝑟 ≤ 𝑋 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) )
25 12 24 syld ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑃 = 𝑄 ) → ( 𝑋 ≠ 0 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) )
26 25 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 = 𝑄 → ( 𝑋 ≠ 0 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) )
27 26 a1i ⊢ ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 = 𝑄 → ( 𝑋 ≠ 0 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) ) )
28 27 com4l ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 = 𝑄 → ( 𝑋 ≠ 0 → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) ) )
29 28 imp4a ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 = 𝑄 → ( ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) )
30 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
31 30 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
32 simpr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
33 1 5 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
34 32 33 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐵 )
35 1 2 3 latleeqj2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑄 ≤ 𝑋 ↔ ( 𝑋 ∨ 𝑄 ) = 𝑋 ) )
36 31 34 8 35 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑄 ≤ 𝑋 ↔ ( 𝑋 ∨ 𝑄 ) = 𝑋 ) )
37 36 biimpa ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑄 ≤ 𝑋 ) → ( 𝑋 ∨ 𝑄 ) = 𝑋 )
38 37 breq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑄 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ↔ 𝑃 ≤ 𝑋 ) )
39 38 biimpa ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑃 ≤ 𝑋 )
40 39 expl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑃 ≤ 𝑋 ) )
41 simpl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
42 simpr2 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
43 2 3 5 hlatlej2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ≤ ( 𝑄 ∨ 𝑃 ) )
44 41 32 42 43 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ≤ ( 𝑄 ∨ 𝑃 ) )
45 40 44 jctird ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑃 ) ) ) )
46 45 42 jctild ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑃 ) ) ) ) )
47 46 impl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑃 ) ) ) )
48 breq1 ⊢ ( 𝑟 = 𝑃 → ( 𝑟 ≤ 𝑋 ↔ 𝑃 ≤ 𝑋 ) )
49 oveq2 ⊢ ( 𝑟 = 𝑃 → ( 𝑄 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑃 ) )
50 49 breq2d ⊢ ( 𝑟 = 𝑃 → ( 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ↔ 𝑃 ≤ ( 𝑄 ∨ 𝑃 ) ) )
51 48 50 anbi12d ⊢ ( 𝑟 = 𝑃 → ( ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ↔ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑃 ) ) ) )
52 51 rspcev ⊢ ( ( 𝑃 ∈ 𝐴 ∧ ( 𝑃 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑃 ) ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) )
53 47 52 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) )
54 53 adantrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑄 ≤ 𝑋 ) ∧ ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) )
55 54 exp31 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑄 ≤ 𝑋 → ( ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) )
56 simpr ⊢ ( ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) )
57 ioran ⊢ ( ¬ ( 𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋 ) ↔ ( ¬ 𝑃 = 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) )
58 df-ne ⊢ ( 𝑃 ≠ 𝑄 ↔ ¬ 𝑃 = 𝑄 )
59 58 anbi1i ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ↔ ( ¬ 𝑃 = 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) )
60 57 59 bitr4i ⊢ ( ¬ ( 𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋 ) ↔ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) )
61 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
62 1 2 3 61 5 cvrat3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) )
63 62 3expd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ≠ 𝑄 → ( ¬ 𝑄 ≤ 𝑋 → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) ) ) )
64 63 imp4c ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ) )
65 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
66 42 65 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐵 )
67 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
68 31 66 34 67 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
69 1 2 61 latmle1 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 )
70 31 8 68 69 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 )
71 70 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 )
72 simpll ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → 𝐾 ∈ HL )
73 63 imp44 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 )
74 simplr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → 𝑃 ∈ 𝐴 )
75 34 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → 𝑄 ∈ 𝐵 )
76 73 74 75 3jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) )
77 72 76 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ) )
78 1 2 61 4 5 atnle ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ¬ 𝑄 ≤ 𝑋 ↔ ( 𝑄 ( meet ‘ 𝐾 ) 𝑋 ) = 0 ) )
79 7 32 8 78 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ¬ 𝑄 ≤ 𝑋 ↔ ( 𝑄 ( meet ‘ 𝐾 ) 𝑋 ) = 0 ) )
80 1 61 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑄 ( meet ‘ 𝐾 ) 𝑋 ) = ( 𝑋 ( meet ‘ 𝐾 ) 𝑄 ) )
81 31 34 8 80 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑄 ( meet ‘ 𝐾 ) 𝑋 ) = ( 𝑋 ( meet ‘ 𝐾 ) 𝑄 ) )
82 81 eqeq1d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑄 ( meet ‘ 𝐾 ) 𝑋 ) = 0 ↔ ( 𝑋 ( meet ‘ 𝐾 ) 𝑄 ) = 0 ) )
83 79 82 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ¬ 𝑄 ≤ 𝑋 ↔ ( 𝑋 ( meet ‘ 𝐾 ) 𝑄 ) = 0 ) )
84 1 61 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 )
85 31 8 68 84 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 )
86 85 8 34 3jca ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) )
87 31 86 jca ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) ) )
88 1 2 61 latmlem2 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ≤ ( 𝑄 ( meet ‘ 𝐾 ) 𝑋 ) ) )
89 87 70 88 sylc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ≤ ( 𝑄 ( meet ‘ 𝐾 ) 𝑋 ) )
90 89 81 breqtrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ≤ ( 𝑋 ( meet ‘ 𝐾 ) 𝑄 ) )
91 breq2 ⊢ ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑄 ) = 0 → ( ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ≤ ( 𝑋 ( meet ‘ 𝐾 ) 𝑄 ) ↔ ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ≤ 0 ) )
92 90 91 syl5ibcom ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑄 ) = 0 → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ≤ 0 ) )
93 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
94 93 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ OP )
95 1 61 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 ) → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ∈ 𝐵 )
96 31 34 85 95 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ∈ 𝐵 )
97 1 2 4 ople0 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ∈ 𝐵 ) → ( ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ≤ 0 ↔ ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = 0 ) )
98 94 96 97 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ≤ 0 ↔ ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = 0 ) )
99 92 98 sylibd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) 𝑄 ) = 0 → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = 0 ) )
100 83 99 sylbid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ¬ 𝑄 ≤ 𝑋 → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = 0 ) )
101 100 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = 0 )
102 101 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ) → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = 0 )
103 102 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = 0 )
104 1 2 61 latmle2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
105 31 8 68 104 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑃 ∨ 𝑄 ) )
106 1 3 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
107 31 66 34 106 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑃 ) )
108 105 107 breqtrd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑄 ∨ 𝑃 ) )
109 108 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑄 ∨ 𝑃 ) )
110 30 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
111 simpr3 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ) → 𝑄 ∈ 𝐵 )
112 simpr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 )
113 1 5 atbase ⊢ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 )
114 112 113 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 )
115 1 61 latmcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐵 ) → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ( meet ‘ 𝐾 ) 𝑄 ) )
116 110 111 114 115 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ) → ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ( meet ‘ 𝐾 ) 𝑄 ) )
117 116 eqeq1d ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ) → ( ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = 0 ↔ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ( meet ‘ 𝐾 ) 𝑄 ) = 0 ) )
118 1 2 3 61 4 5 hlexch3 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ( meet ‘ 𝐾 ) 𝑄 ) = 0 ) → ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑄 ∨ 𝑃 ) → 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) )
119 118 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ) → ( ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ( meet ‘ 𝐾 ) 𝑄 ) = 0 → ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑄 ∨ 𝑃 ) → 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) ) )
120 117 119 sylbid ⊢ ( ( 𝐾 ∈ HL ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ) → ( ( 𝑄 ( meet ‘ 𝐾 ) ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) = 0 → ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ ( 𝑄 ∨ 𝑃 ) → 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) ) )
121 77 103 109 120 syl3c ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) )
122 71 121 jca ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) )
123 122 ex ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) ) )
124 64 123 jcad ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) ) ) )
125 breq1 ⊢ ( 𝑟 = ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → ( 𝑟 ≤ 𝑋 ↔ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 ) )
126 oveq2 ⊢ ( 𝑟 = ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → ( 𝑄 ∨ 𝑟 ) = ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) )
127 126 breq2d ⊢ ( 𝑟 = ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ↔ 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) )
128 125 127 anbi12d ⊢ ( 𝑟 = ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → ( ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ↔ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) ) )
129 128 rspcev ⊢ ( ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ∈ 𝐴 ∧ ( ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ ( 𝑋 ( meet ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) )
130 124 129 syl6 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) )
131 130 expd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) )
132 60 131 biimtrid ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ¬ ( 𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) )
133 56 132 syl7 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ¬ ( 𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋 ) → ( ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) ) )
134 29 55 133 ecase3d ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ( 𝑋 ≠ 0 ∧ 𝑃 ≤ ( 𝑋 ∨ 𝑄 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) ) )