Step |
Hyp |
Ref |
Expression |
1 |
|
paddasslem.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
paddasslem.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
paddasslem.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
paddasslem.p |
⊢ + = ( +𝑃 ‘ 𝐾 ) |
5 |
|
simpl1l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝐾 ∈ HL ) |
6 |
|
simpl21 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑋 ⊆ 𝐴 ) |
7 |
|
simpl22 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑌 ⊆ 𝐴 ) |
8 |
3 4
|
paddssat |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 ) |
9 |
5 6 7 8
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 ) |
10 |
|
simpl23 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑍 ⊆ 𝐴 ) |
11 |
3 4
|
sspadd1 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) |
12 |
5 9 10 11
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑋 + 𝑌 ) ⊆ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) |
13 |
5
|
hllatd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝐾 ∈ Lat ) |
14 |
|
simprll |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑥 ∈ 𝑋 ) |
15 |
|
simprlr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑦 ∈ 𝑌 ) |
16 |
|
simpl3l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ∈ 𝐴 ) |
17 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
18 |
17 3
|
atbase |
⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) ) |
19 |
16 18
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ∈ ( Base ‘ 𝐾 ) ) |
20 |
6 14
|
sseldd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑥 ∈ 𝐴 ) |
21 |
17 3
|
atbase |
⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( Base ‘ 𝐾 ) ) |
22 |
20 21
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐾 ) ) |
23 |
|
simpl3r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑟 ∈ 𝐴 ) |
24 |
17 3
|
atbase |
⊢ ( 𝑟 ∈ 𝐴 → 𝑟 ∈ ( Base ‘ 𝐾 ) ) |
25 |
23 24
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) ) |
26 |
17 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) ) |
27 |
13 22 25 26
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑥 ∨ 𝑟 ) ∈ ( Base ‘ 𝐾 ) ) |
28 |
7 15
|
sseldd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑦 ∈ 𝐴 ) |
29 |
17 3
|
atbase |
⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( Base ‘ 𝐾 ) ) |
30 |
28 29
|
syl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑦 ∈ ( Base ‘ 𝐾 ) ) |
31 |
17 2
|
latjcl |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) |
32 |
13 22 30 31
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) |
33 |
|
simprrr |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) |
34 |
17 1 2
|
latlej1 |
⊢ ( ( 𝐾 ∈ Lat ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝑥 ≤ ( 𝑥 ∨ 𝑦 ) ) |
35 |
13 22 30 34
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑥 ≤ ( 𝑥 ∨ 𝑦 ) ) |
36 |
|
simprrl |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) |
37 |
17 1 2
|
latjle12 |
⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑥 ∨ 𝑦 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑥 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ↔ ( 𝑥 ∨ 𝑟 ) ≤ ( 𝑥 ∨ 𝑦 ) ) ) |
38 |
13 22 25 32 37
|
syl13anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( ( 𝑥 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ) ↔ ( 𝑥 ∨ 𝑟 ) ≤ ( 𝑥 ∨ 𝑦 ) ) ) |
39 |
35 36 38
|
mpbi2and |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → ( 𝑥 ∨ 𝑟 ) ≤ ( 𝑥 ∨ 𝑦 ) ) |
40 |
17 1 13 19 27 32 33 39
|
lattrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ≤ ( 𝑥 ∨ 𝑦 ) ) |
41 |
1 2 3 4
|
elpaddri |
⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑦 ) ) ) → 𝑝 ∈ ( 𝑋 + 𝑌 ) ) |
42 |
13 6 7 14 15 16 40 41
|
syl322anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ∈ ( 𝑋 + 𝑌 ) ) |
43 |
12 42
|
sseldd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ) ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑟 ≤ ( 𝑥 ∨ 𝑦 ) ∧ 𝑝 ≤ ( 𝑥 ∨ 𝑟 ) ) ) ) → 𝑝 ∈ ( ( 𝑋 + 𝑌 ) + 𝑍 ) ) |