Step |
Hyp |
Ref |
Expression |
1 |
|
3dim0.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
2 |
|
3dim0.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
3dim0.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
1 2 3
|
3dim2 |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) |
5 |
4
|
3adant3r1 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) |
6 |
|
simpl2l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → 𝑣 ∈ 𝐴 ) |
7 |
|
simp3l |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ) |
8 |
|
simp1l |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝐾 ∈ HL ) |
9 |
|
simp1r2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑄 ∈ 𝐴 ) |
10 |
1 3
|
hlatjidm |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 ) |
11 |
8 9 10
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝑄 ∨ 𝑄 ) = 𝑄 ) |
12 |
11
|
oveq1d |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) |
13 |
12
|
breq2d |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ) ) |
14 |
7 13
|
mtbird |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ¬ 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ) |
15 |
|
oveq1 |
⊢ ( 𝑃 = 𝑄 → ( 𝑃 ∨ 𝑄 ) = ( 𝑄 ∨ 𝑄 ) ) |
16 |
15
|
oveq1d |
⊢ ( 𝑃 = 𝑄 → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ) |
17 |
16
|
breq2d |
⊢ ( 𝑃 = 𝑄 → ( 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ) ) |
18 |
17
|
notbid |
⊢ ( 𝑃 = 𝑄 → ( ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ¬ 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ) ) |
19 |
18
|
biimparc |
⊢ ( ( ¬ 𝑣 ≤ ( ( 𝑄 ∨ 𝑄 ) ∨ 𝑅 ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
20 |
14 19
|
sylan |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
21 |
|
breq1 |
⊢ ( 𝑠 = 𝑣 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) |
22 |
21
|
notbid |
⊢ ( 𝑠 = 𝑣 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) |
23 |
22
|
rspcev |
⊢ ( ( 𝑣 ∈ 𝐴 ∧ ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
24 |
6 20 23
|
syl2anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 = 𝑄 ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
25 |
|
simp2l |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑣 ∈ 𝐴 ) |
26 |
25
|
ad2antrr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → 𝑣 ∈ 𝐴 ) |
27 |
7
|
ad2antrr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ) |
28 |
1 3
|
hlatjass |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) ) |
29 |
28
|
3ad2ant1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) ) |
30 |
29
|
ad2antrr |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) ) |
31 |
8
|
hllatd |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝐾 ∈ Lat ) |
32 |
|
simp1r1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑃 ∈ 𝐴 ) |
33 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
34 |
33 3
|
atbase |
⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) ) |
35 |
32 34
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) ) |
36 |
|
simp1r3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → 𝑅 ∈ 𝐴 ) |
37 |
33 1 3
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) |
38 |
8 9 36 37
|
syl3anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) |
39 |
31 35 38
|
3jca |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) |
40 |
39
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) |
41 |
33 2 1
|
latleeqj1 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) = ( 𝑄 ∨ 𝑅 ) ) ) |
42 |
40 41
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ( 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ↔ ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) = ( 𝑄 ∨ 𝑅 ) ) ) |
43 |
42
|
biimpa |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑃 ∨ ( 𝑄 ∨ 𝑅 ) ) = ( 𝑄 ∨ 𝑅 ) ) |
44 |
30 43
|
eqtrd |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) |
45 |
44
|
breq2d |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ( 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ) ) |
46 |
27 45
|
mtbird |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
47 |
26 46 23
|
syl2anc |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
48 |
|
simpl2r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑤 ∈ 𝐴 ) |
49 |
48
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → 𝑤 ∈ 𝐴 ) |
50 |
8 32 9
|
3jca |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) |
51 |
50
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) |
52 |
36 25
|
jca |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) |
53 |
52
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) |
54 |
|
simpl3r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) |
55 |
54
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) |
56 |
|
simplr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) |
57 |
|
simpr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) |
58 |
1 2 3
|
3dimlem3a |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
59 |
51 53 55 56 57 58
|
syl113anc |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
60 |
|
breq1 |
⊢ ( 𝑠 = 𝑤 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) |
61 |
60
|
notbid |
⊢ ( 𝑠 = 𝑤 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ↔ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) |
62 |
61
|
rspcev |
⊢ ( ( 𝑤 ∈ 𝐴 ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
63 |
49 59 62
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
64 |
|
simpl2l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → 𝑣 ∈ 𝐴 ) |
65 |
64
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → 𝑣 ∈ 𝐴 ) |
66 |
50
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ) |
67 |
52
|
ad3antrrr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ) |
68 |
|
simpl3l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ) |
69 |
68
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ) |
70 |
|
simplr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) |
71 |
|
simpr |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) |
72 |
1 2 3
|
3dimlem4a |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
73 |
66 67 69 70 71 72
|
syl113anc |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ¬ 𝑣 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
74 |
65 73 23
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ∧ ¬ 𝑃 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
75 |
63 74
|
pm2.61dan |
⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) ∧ ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
76 |
47 75
|
pm2.61dan |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
77 |
24 76
|
pm2.61dane |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |
78 |
77
|
3exp |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) ) |
79 |
78
|
rexlimdvv |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ( ∃ 𝑣 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ¬ 𝑣 ≤ ( 𝑄 ∨ 𝑅 ) ∧ ¬ 𝑤 ≤ ( ( 𝑄 ∨ 𝑅 ) ∨ 𝑣 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) ) |
80 |
5 79
|
mpd |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ) → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑄 ) ∨ 𝑅 ) ) |