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

Metamath Proof Explorer

Theorem cvratlem

Description: Lemma for cvrat . ( atcvatlem analog.) (Contributed by NM, 22-Nov-2011)

Ref Expression
Hypotheses cvrat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrat.s ⊢ < = ( lt ‘ 𝐾 )
cvrat.j ⊢ ∨ = ( join ‘ 𝐾 )
cvrat.z ⊢ 0 = ( 0. ‘ 𝐾 )
cvrat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvratlem ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cvrat.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrat.s ⊢ < = ( lt ‘ 𝐾 )
3 cvrat.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvrat.z ⊢ 0 = ( 0. ‘ 𝐾 )
5 cvrat.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
7 6 adantr ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝐾 ∈ AtLat )
8 simpr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → 𝑋 ∈ 𝐵 )
9 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
10 1 9 4 5 atlex ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃ 𝑟 ∈ 𝐴 𝑟 ( le ‘ 𝐾 ) 𝑋 )
11 10 3expia ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ≠ 0 → ∃ 𝑟 ∈ 𝐴 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
12 7 8 11 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ≠ 0 → ∃ 𝑟 ∈ 𝐴 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
13 6 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
14 simp22 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
15 simp3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑟 ∈ 𝐴 )
16 9 5 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ( le ‘ 𝐾 ) 𝑟 ↔ 𝑃 = 𝑟 ) )
17 13 14 15 16 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ( le ‘ 𝐾 ) 𝑟 ↔ 𝑃 = 𝑟 ) )
18 breq1 ⊢ ( 𝑃 = 𝑟 → ( 𝑃 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑟 ( le ‘ 𝐾 ) 𝑋 ) )
19 18 biimprd ⊢ ( 𝑃 = 𝑟 → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → 𝑃 ( le ‘ 𝐾 ) 𝑋 ) )
20 17 19 biimtrdi ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ( le ‘ 𝐾 ) 𝑟 → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) )
21 20 com23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → ( 𝑃 ( le ‘ 𝐾 ) 𝑟 → 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) )
22 con3 ⊢ ( ( 𝑃 ( le ‘ 𝐾 ) 𝑟 → 𝑃 ( le ‘ 𝐾 ) 𝑋 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → ¬ 𝑃 ( le ‘ 𝐾 ) 𝑟 ) )
23 21 22 syl6 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → ¬ 𝑃 ( le ‘ 𝐾 ) 𝑟 ) ) )
24 23 impd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) → ¬ 𝑃 ( le ‘ 𝐾 ) 𝑟 ) )
25 simp1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ HL )
26 1 5 atbase ⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵 )
27 26 3ad2ant3 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑟 ∈ 𝐵 )
28 eqid ⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 )
29 1 9 3 28 5 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑟 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑟 ↔ 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑟 ∨ 𝑃 ) ) )
30 25 27 14 29 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑟 ↔ 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑟 ∨ 𝑃 ) ) )
31 24 30 sylibd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) → 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑟 ∨ 𝑃 ) ) )
32 31 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑟 ∨ 𝑃 ) )
33 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
34 33 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ Lat )
35 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
36 14 35 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
37 1 3 latjcom ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑟 ) = ( 𝑟 ∨ 𝑃 ) )
38 34 36 27 37 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑟 ) = ( 𝑟 ∨ 𝑃 ) )
39 38 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) → ( 𝑃 ∨ 𝑟 ) = ( 𝑟 ∨ 𝑃 ) )
40 32 39 breqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) → 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) )
41 40 adantrrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) )
42 9 3 5 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) )
43 25 14 15 42 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) )
44 43 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) )
45 9 5 atcmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑃 ↔ 𝑟 = 𝑃 ) )
46 13 15 14 45 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑃 ↔ 𝑟 = 𝑃 ) )
47 breq1 ⊢ ( 𝑟 = 𝑃 → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) )
48 47 biimpd ⊢ ( 𝑟 = 𝑃 → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → 𝑃 ( le ‘ 𝐾 ) 𝑋 ) )
49 46 48 biimtrdi ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑃 → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) )
50 49 com23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → ( 𝑟 ( le ‘ 𝐾 ) 𝑃 → 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) )
51 con3 ⊢ ( ( 𝑟 ( le ‘ 𝐾 ) 𝑃 → 𝑃 ( le ‘ 𝐾 ) 𝑋 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → ¬ 𝑟 ( le ‘ 𝐾 ) 𝑃 ) )
52 50 51 syl6 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → ¬ 𝑟 ( le ‘ 𝐾 ) 𝑃 ) ) )
53 52 imp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) → ¬ 𝑟 ( le ‘ 𝐾 ) 𝑃 )
54 53 adantrrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ¬ 𝑟 ( le ‘ 𝐾 ) 𝑃 )
55 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → 𝑟 ( le ‘ 𝐾 ) 𝑋 )
56 simp21 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
57 simp23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
58 1 5 atbase ⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵 )
59 57 58 syl ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑄 ∈ 𝐵 )
60 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
61 34 36 59 60 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 )
62 25 56 61 3jca ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) )
63 9 2 pltle ⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
64 63 imp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
65 62 64 sylan ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
66 65 adantrl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → 𝑋 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
67 hlpos ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
68 67 3ad2ant1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ Poset )
69 1 9 postr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑟 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
70 68 27 56 61 69 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
71 70 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
72 55 66 71 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
73 72 adantrrr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
74 1 9 3 5 hlexch1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵 ) ∧ ¬ 𝑟 ( le ‘ 𝐾 ) 𝑃 ) → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) )
75 74 3expia ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵 ) ) → ( ¬ 𝑟 ( le ‘ 𝐾 ) 𝑃 → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) ) )
76 75 impd ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵 ) ) → ( ( ¬ 𝑟 ( le ‘ 𝐾 ) 𝑃 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) )
77 25 15 57 36 76 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ( ¬ 𝑟 ( le ‘ 𝐾 ) 𝑃 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) )
78 77 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( ( ¬ 𝑟 ( le ‘ 𝐾 ) 𝑃 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) )
79 54 73 78 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) )
80 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ) → ( 𝑃 ∨ 𝑟 ) ∈ 𝐵 )
81 34 36 27 80 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑟 ) ∈ 𝐵 )
82 1 9 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑟 ) ∈ 𝐵 ) ) → ( ( 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) )
83 34 36 59 81 82 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) )
84 83 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( ( 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ∧ 𝑄 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) )
85 44 79 84 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) )
86 9 3 5 hlatlej1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
87 25 14 57 86 syl3anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
88 87 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
89 1 9 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ) ) → ( ( 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑃 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
90 34 36 27 61 89 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑃 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
91 90 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( ( 𝑃 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑃 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
92 88 73 91 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( 𝑃 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) )
93 34 61 81 3jca ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑟 ) ∈ 𝐵 ) )
94 93 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑟 ) ∈ 𝐵 ) )
95 1 9 latasymb ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑟 ) ∈ 𝐵 ) → ( ( ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ∧ ( 𝑃 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑟 ) ) )
96 94 95 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( ( ( 𝑃 ∨ 𝑄 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ∧ ( 𝑃 ∨ 𝑟 ) ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑟 ) ) )
97 85 92 96 mpbi2and ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑟 ) )
98 breq2 ⊢ ( ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑟 ) → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ↔ 𝑋 < ( 𝑃 ∨ 𝑟 ) ) )
99 98 biimpcd ⊢ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → ( ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑟 ) → 𝑋 < ( 𝑃 ∨ 𝑟 ) ) )
100 99 adantr ⊢ ( ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) → ( ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑟 ) → 𝑋 < ( 𝑃 ∨ 𝑟 ) ) )
101 100 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑟 ) → 𝑋 < ( 𝑃 ∨ 𝑟 ) ) )
102 97 101 mpd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → 𝑋 < ( 𝑃 ∨ 𝑟 ) )
103 1 9 2 28 cvrnbtwn3 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑟 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑟 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 < ( 𝑃 ∨ 𝑟 ) ) ↔ 𝑟 = 𝑋 ) )
104 103 biimpd ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑟 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑟 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ) → ( ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 < ( 𝑃 ∨ 𝑟 ) ) → 𝑟 = 𝑋 ) )
105 104 3expia ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑟 ∈ 𝐵 ∧ ( 𝑃 ∨ 𝑟 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) → ( ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 < ( 𝑃 ∨ 𝑟 ) ) → 𝑟 = 𝑋 ) ) )
106 68 27 81 56 105 syl13anc ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) → ( ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑋 < ( 𝑃 ∨ 𝑟 ) ) → 𝑟 = 𝑋 ) ) )
107 106 exp4a ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → ( 𝑋 < ( 𝑃 ∨ 𝑟 ) → 𝑟 = 𝑋 ) ) ) )
108 107 com23 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → ( 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) → ( 𝑋 < ( 𝑃 ∨ 𝑟 ) → 𝑟 = 𝑋 ) ) ) )
109 108 imp4b ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ 𝑟 ( le ‘ 𝐾 ) 𝑋 ) → ( ( 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ∧ 𝑋 < ( 𝑃 ∨ 𝑟 ) ) → 𝑟 = 𝑋 ) )
110 109 adantrr ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → ( ( 𝑟 ( ⋖ ‘ 𝐾 ) ( 𝑃 ∨ 𝑟 ) ∧ 𝑋 < ( 𝑃 ∨ 𝑟 ) ) → 𝑟 = 𝑋 ) )
111 41 102 110 mp2and ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → 𝑟 = 𝑋 )
112 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → 𝑟 ∈ 𝐴 )
113 111 112 eqeltrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑟 ( le ‘ 𝐾 ) 𝑋 ∧ ( 𝑋 < ( 𝑃 ∨ 𝑄 ) ∧ ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 ) ) ) → 𝑋 ∈ 𝐴 )
114 113 exp45 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) ) ) )
115 114 3expa ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑟 ( le ‘ 𝐾 ) 𝑋 → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) ) ) )
116 115 rexlimdva ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( ∃ 𝑟 ∈ 𝐴 𝑟 ( le ‘ 𝐾 ) 𝑋 → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) ) ) )
117 12 116 syld ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) → ( 𝑋 ≠ 0 → ( 𝑋 < ( 𝑃 ∨ 𝑄 ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) ) ) )
118 117 imp32 ⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) ∧ ( 𝑋 ≠ 0 ∧ 𝑋 < ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑃 ( le ‘ 𝐾 ) 𝑋 → 𝑋 ∈ 𝐴 ) )