Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝐾 ∈ HL) |
2 | | hllat 34650 |
. . . 4
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝐾 ∈ Lat) |
4 | | simpl2 1065 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑋 ⊆ 𝐴) |
5 | | simpl3 1066 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑝 ∈ 𝐴) |
6 | | simprl 794 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑋 ≠ ∅) |
7 | | inss2 3834 |
. . . . . 6
⊢ (( ⊥
‘𝑋) ∩ 𝑀) ⊆ 𝑀 |
8 | 7 | sseli 3599 |
. . . . 5
⊢ (𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀) → 𝑞 ∈ 𝑀) |
9 | | pexmidlem.m |
. . . . 5
⊢ 𝑀 = (𝑋 + {𝑝}) |
10 | 8, 9 | syl6eleq 2711 |
. . . 4
⊢ (𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀) → 𝑞 ∈ (𝑋 + {𝑝})) |
11 | 10 | ad2antll 765 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑞 ∈ (𝑋 + {𝑝})) |
12 | | pexmidlem.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
13 | | pexmidlem.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
14 | | pexmidlem.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
15 | | pexmidlem.p |
. . . 4
⊢ + =
(+𝑃‘𝐾) |
16 | 12, 13, 14, 15 | elpaddatiN 35091 |
. . 3
⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (𝑋 + {𝑝}))) → ∃𝑟 ∈ 𝑋 𝑞 ≤ (𝑟 ∨ 𝑝)) |
17 | 3, 4, 5, 6, 11, 16 | syl32anc 1334 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → ∃𝑟 ∈ 𝑋 𝑞 ≤ (𝑟 ∨ 𝑝)) |
18 | | simp1 1061 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → (𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴)) |
19 | | simp3l 1089 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑟 ∈ 𝑋) |
20 | | inss1 3833 |
. . . . . . 7
⊢ (( ⊥
‘𝑋) ∩ 𝑀) ⊆ ( ⊥ ‘𝑋) |
21 | | simp2r 1088 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀)) |
22 | 20, 21 | sseldi 3601 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑞 ∈ ( ⊥ ‘𝑋)) |
23 | | simp3r 1090 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑞 ≤ (𝑟 ∨ 𝑝)) |
24 | | pexmidlem.o |
. . . . . . 7
⊢ ⊥ =
(⊥𝑃‘𝐾) |
25 | 12, 13, 14, 15, 24, 9 | pexmidlem3N 35258 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋)) ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) |
26 | 18, 19, 22, 23, 25 | syl121anc 1331 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) |
27 | 26 | 3expia 1267 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → ((𝑟 ∈ 𝑋 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) |
28 | 27 | expd 452 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → (𝑟 ∈ 𝑋 → (𝑞 ≤ (𝑟 ∨ 𝑝) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))))) |
29 | 28 | rexlimdv 3030 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → (∃𝑟 ∈ 𝑋 𝑞 ≤ (𝑟 ∨ 𝑝) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) |
30 | 17, 29 | mpd 15 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) |