| Step |
Hyp |
Ref |
Expression |
| 1 |
|
llncvrlpln2.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
| 2 |
|
llncvrlpln2.c |
⊢ 𝐶 = ( ⋖ ‘ 𝐾 ) |
| 3 |
|
llncvrlpln2.n |
⊢ 𝑁 = ( LLines ‘ 𝐾 ) |
| 4 |
|
llncvrlpln2.p |
⊢ 𝑃 = ( LPlanes ‘ 𝐾 ) |
| 5 |
|
simpr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 ) |
| 6 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ HL ) |
| 7 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ 𝑃 ) |
| 8 |
3 4
|
lplnnelln |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑌 ∈ 𝑃 ) → ¬ 𝑌 ∈ 𝑁 ) |
| 9 |
6 7 8
|
syl2anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → ¬ 𝑌 ∈ 𝑁 ) |
| 10 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ 𝑁 ) |
| 11 |
|
eleq1 |
⊢ ( 𝑋 = 𝑌 → ( 𝑋 ∈ 𝑁 ↔ 𝑌 ∈ 𝑁 ) ) |
| 12 |
10 11
|
syl5ibcom |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 = 𝑌 → 𝑌 ∈ 𝑁 ) ) |
| 13 |
12
|
necon3bd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → ( ¬ 𝑌 ∈ 𝑁 → 𝑋 ≠ 𝑌 ) ) |
| 14 |
9 13
|
mpd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≠ 𝑌 ) |
| 15 |
|
eqid |
⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 ) |
| 16 |
1 15
|
pltval |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) ) |
| 17 |
16
|
adantr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) ) |
| 18 |
5 14 17
|
mpbir2and |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) |
| 19 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝐾 ∈ HL ) |
| 20 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ∈ 𝑁 ) |
| 21 |
|
eqid |
⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) |
| 22 |
21 3
|
llnbase |
⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ ( Base ‘ 𝐾 ) ) |
| 23 |
20 22
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ∈ ( Base ‘ 𝐾 ) ) |
| 24 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑌 ∈ 𝑃 ) |
| 25 |
21 4
|
lplnbase |
⊢ ( 𝑌 ∈ 𝑃 → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
| 26 |
24 25
|
syl |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝐾 ) ) |
| 27 |
|
simpr |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) |
| 28 |
|
eqid |
⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 ) |
| 29 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
| 30 |
21 1 15 28 2 29
|
hlrelat3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ 𝑌 ∈ ( Base ‘ 𝐾 ) ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) |
| 31 |
19 23 26 27 30
|
syl31anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) |
| 32 |
21 1 28 29 4
|
islpln2 |
⊢ ( 𝐾 ∈ HL → ( 𝑌 ∈ 𝑃 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) ) ) |
| 33 |
32
|
adantr |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → ( 𝑌 ∈ 𝑃 ↔ ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) ) ) |
| 34 |
|
simp3 |
⊢ ( ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) |
| 35 |
21 28 29 3
|
islln2 |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) ) ) |
| 36 |
|
simp3l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ) |
| 37 |
|
simp3r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) |
| 38 |
|
simp12r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) |
| 39 |
38
|
oveq1d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) |
| 40 |
|
simp22 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) |
| 41 |
37 39 40
|
3brtr3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ≤ ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) |
| 42 |
|
simp111 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝐾 ∈ HL ) |
| 43 |
|
simp112 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) |
| 44 |
|
simp113 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) |
| 45 |
|
simp23 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) |
| 46 |
43 44 45
|
3jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ) |
| 47 |
|
simp13l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑠 ∈ ( Atoms ‘ 𝐾 ) ) |
| 48 |
|
simp13r |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) |
| 49 |
|
simp21 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) |
| 50 |
47 48 49
|
3jca |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) |
| 51 |
36 38 39
|
3brtr3d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) |
| 52 |
21 28 29
|
hlatjcl |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) |
| 53 |
42 43 44 52
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ) |
| 54 |
21 1 28 2 29
|
cvr1 |
⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) |
| 55 |
42 53 45 54
|
syl3anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ↔ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) 𝐶 ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ) ) |
| 56 |
51 55
|
mpbird |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) |
| 57 |
|
simp12l |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑝 ≠ 𝑞 ) |
| 58 |
1 28 29
|
3at |
⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( ¬ 𝑟 ≤ ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ∧ 𝑝 ≠ 𝑞 ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ≤ ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) |
| 59 |
42 46 50 56 57 58
|
syl32anc |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) ≤ ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ↔ ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) |
| 60 |
41 59
|
mpbid |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ( join ‘ 𝐾 ) 𝑟 ) = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) |
| 61 |
60 39 40
|
3eqtr4d |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) = 𝑌 ) |
| 62 |
36 61
|
breqtrd |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑋 𝐶 𝑌 ) |
| 63 |
62
|
3exp |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) |
| 64 |
63
|
3expd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) |
| 65 |
64
|
3exp |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) |
| 66 |
65
|
3expib |
⊢ ( 𝐾 ∈ HL → ( ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) ) |
| 67 |
66
|
rexlimdvv |
⊢ ( 𝐾 ∈ HL → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) |
| 68 |
67
|
adantld |
⊢ ( 𝐾 ∈ HL → ( ( 𝑋 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( 𝑝 ≠ 𝑞 ∧ 𝑋 = ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) ) ) → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) |
| 69 |
35 68
|
sylbid |
⊢ ( 𝐾 ∈ HL → ( 𝑋 ∈ 𝑁 → ( ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) ) ) |
| 70 |
69
|
imp31 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) |
| 71 |
34 70
|
syl7 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( 𝑢 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) ) |
| 72 |
71
|
rexlimdv |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) ∧ ( 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ) ) → ( ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) |
| 73 |
72
|
rexlimdvva |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → ( ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) |
| 74 |
73
|
adantld |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → ( ( 𝑌 ∈ ( Base ‘ 𝐾 ) ∧ ∃ 𝑠 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑡 ∈ ( Atoms ‘ 𝐾 ) ∃ 𝑢 ∈ ( Atoms ‘ 𝐾 ) ( 𝑠 ≠ 𝑡 ∧ ¬ 𝑢 ≤ ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ∧ 𝑌 = ( ( 𝑠 ( join ‘ 𝐾 ) 𝑡 ) ( join ‘ 𝐾 ) 𝑢 ) ) ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) |
| 75 |
33 74
|
sylbid |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ) → ( 𝑌 ∈ 𝑃 → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) ) |
| 76 |
75
|
3impia |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) → ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → ( ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) ) |
| 77 |
76
|
rexlimdv |
⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) ) |
| 78 |
77
|
imp |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ( 𝑋 𝐶 ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ∧ ( 𝑋 ( join ‘ 𝐾 ) 𝑟 ) ≤ 𝑌 ) ) → 𝑋 𝐶 𝑌 ) |
| 79 |
31 78
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ( lt ‘ 𝐾 ) 𝑌 ) → 𝑋 𝐶 𝑌 ) |
| 80 |
18 79
|
syldan |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) |