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 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃 ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 𝐶 𝑌 ) |