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