Step |
Hyp |
Ref |
Expression |
1 |
|
2llnj.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
2 |
|
2llnj.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
3 |
|
2llnj.n |
⊢ 𝑁 = ( LLines ‘ 𝐾 ) |
4 |
|
2llnj.p |
⊢ 𝑃 = ( LPlanes ‘ 𝐾 ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
6 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
7 |
5 2 6 3
|
islln2 |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ) ) |
8 |
|
simpr |
⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) |
9 |
7 8
|
syl6bi |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 → ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ) |
10 |
5 2 6 3
|
islln2 |
⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑁 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) ) |
11 |
|
simpr |
⊢ ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) |
12 |
10 11
|
syl6bi |
⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑁 → ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) |
13 |
9 12
|
anim12d |
⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) ) |
14 |
13
|
imp |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) |
15 |
14
|
3adantr3 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) |
16 |
15
|
3adant3 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) |
17 |
|
simp2rr |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑋 = ( 𝑞 ∨ 𝑟 ) ) |
18 |
|
simp3rr |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑌 = ( 𝑠 ∨ 𝑡 ) ) |
19 |
17 18
|
oveq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( 𝑋 ∨ 𝑌 ) = ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) ) |
20 |
|
simp13 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) |
21 |
|
breq1 |
⊢ ( 𝑋 = ( 𝑞 ∨ 𝑟 ) → ( 𝑋 ≤ 𝑊 ↔ ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ) ) |
22 |
|
neeq1 |
⊢ ( 𝑋 = ( 𝑞 ∨ 𝑟 ) → ( 𝑋 ≠ 𝑌 ↔ ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ) ) |
23 |
21 22
|
3anbi13d |
⊢ ( 𝑋 = ( 𝑞 ∨ 𝑟 ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ) ) ) |
24 |
|
breq1 |
⊢ ( 𝑌 = ( 𝑠 ∨ 𝑡 ) → ( 𝑌 ≤ 𝑊 ↔ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ) ) |
25 |
|
neeq2 |
⊢ ( 𝑌 = ( 𝑠 ∨ 𝑡 ) → ( ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ↔ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) |
26 |
24 25
|
3anbi23d |
⊢ ( 𝑌 = ( 𝑠 ∨ 𝑡 ) → ( ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) ) |
27 |
23 26
|
sylan9bb |
⊢ ( ( 𝑋 = ( 𝑞 ∨ 𝑟 ) ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) ) |
28 |
17 18 27
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ↔ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) ) |
29 |
20 28
|
mpbid |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) |
30 |
|
simp11 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝐾 ∈ HL ) |
31 |
|
simp123 |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑊 ∈ 𝑃 ) |
32 |
|
simp2ll |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) |
33 |
|
simp2lr |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) |
34 |
|
simp2rl |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑞 ≠ 𝑟 ) |
35 |
|
simp3ll |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) |
36 |
|
simp3lr |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) |
37 |
|
simp3rl |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → 𝑠 ≠ 𝑡 ) |
38 |
1 2 6 3 4
|
2llnjaN |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ≠ 𝑟 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ≠ 𝑡 ) ) ∧ ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 ) |
39 |
38
|
ex |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ≠ 𝑟 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 ≠ 𝑡 ) ) → ( ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 ) ) |
40 |
30 31 32 33 34 35 36 37 39
|
syl233anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( ( 𝑞 ∨ 𝑟 ) ≤ 𝑊 ∧ ( 𝑠 ∨ 𝑡 ) ≤ 𝑊 ∧ ( 𝑞 ∨ 𝑟 ) ≠ ( 𝑠 ∨ 𝑡 ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 ) ) |
41 |
29 40
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( ( 𝑞 ∨ 𝑟 ) ∨ ( 𝑠 ∨ 𝑡 ) ) = 𝑊 ) |
42 |
19 41
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) ∧ ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) |
43 |
42
|
3exp |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) ) |
44 |
43
|
3impib |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) |
45 |
44
|
expd |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) ) |
46 |
45
|
rexlimdvv |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) ∧ ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) |
47 |
46
|
3exp |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) ) ) |
48 |
47
|
rexlimdvv |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) ) |
49 |
48
|
impd |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑞 ≠ 𝑟 ∧ 𝑋 = ( 𝑞 ∨ 𝑟 ) ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ 𝑌 = ( 𝑠 ∨ 𝑡 ) ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) ) |
50 |
16 49
|
mpd |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃 ) ∧ ( 𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌 ) ) → ( 𝑋 ∨ 𝑌 ) = 𝑊 ) |