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 syl6bi ( ( 𝐾 ∈ 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 syl6bi ( ( 𝐾 ∈ 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 ‘ 𝐾 ) 𝑋𝑋𝐴 ) )