Step | Hyp | Ref
| Expression |
1 | | snssi 4735 |
. . . . . 6
⊢ (𝑃 ∈ 𝐴 → {𝑃} ⊆ 𝐴) |
2 | 1 | adantl 485 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → {𝑃} ⊆ 𝐴) |
3 | | atllat 37077 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat) |
4 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(Base‘𝐾) =
(Base‘𝐾) |
5 | | snpsub.a |
. . . . . . . . . . . . . . . 16
⊢ 𝐴 = (Atoms‘𝐾) |
6 | 4, 5 | atbase 37066 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾)) |
7 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(join‘𝐾) =
(join‘𝐾) |
8 | 4, 7 | latjidm 17992 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ (Base‘𝐾)) → (𝑃(join‘𝐾)𝑃) = 𝑃) |
9 | 3, 6, 8 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → (𝑃(join‘𝐾)𝑃) = 𝑃) |
10 | 9 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃(join‘𝐾)𝑃) = 𝑃) |
11 | 10 | breq2d 5079 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃) ↔ 𝑟(le‘𝐾)𝑃)) |
12 | | eqid 2738 |
. . . . . . . . . . . . . . . 16
⊢
(le‘𝐾) =
(le‘𝐾) |
13 | 12, 5 | atcmp 37088 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ AtLat ∧ 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃)) |
14 | 13 | 3com23 1128 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃)) |
15 | 14 | 3expa 1120 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃)) |
16 | 15 | biimpd 232 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 → 𝑟 = 𝑃)) |
17 | 11, 16 | sylbid 243 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃) → 𝑟 = 𝑃)) |
18 | 17 | adantld 494 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (((𝑝 = 𝑃 ∧ 𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃)) → 𝑟 = 𝑃)) |
19 | | velsn 4571 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ {𝑃} ↔ 𝑝 = 𝑃) |
20 | | velsn 4571 |
. . . . . . . . . . . . 13
⊢ (𝑞 ∈ {𝑃} ↔ 𝑞 = 𝑃) |
21 | 19, 20 | anbi12i 630 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) ↔ (𝑝 = 𝑃 ∧ 𝑞 = 𝑃)) |
22 | 21 | anbi1i 627 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) ↔ ((𝑝 = 𝑃 ∧ 𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞))) |
23 | | oveq12 7240 |
. . . . . . . . . . . . 13
⊢ ((𝑝 = 𝑃 ∧ 𝑞 = 𝑃) → (𝑝(join‘𝐾)𝑞) = (𝑃(join‘𝐾)𝑃)) |
24 | 23 | breq2d 5079 |
. . . . . . . . . . . 12
⊢ ((𝑝 = 𝑃 ∧ 𝑞 = 𝑃) → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) ↔ 𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃))) |
25 | 24 | pm5.32i 578 |
. . . . . . . . . . 11
⊢ (((𝑝 = 𝑃 ∧ 𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) ↔ ((𝑝 = 𝑃 ∧ 𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃))) |
26 | 22, 25 | bitri 278 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) ↔ ((𝑝 = 𝑃 ∧ 𝑞 = 𝑃) ∧ 𝑟(le‘𝐾)(𝑃(join‘𝐾)𝑃))) |
27 | | velsn 4571 |
. . . . . . . . . 10
⊢ (𝑟 ∈ {𝑃} ↔ 𝑟 = 𝑃) |
28 | 18, 26, 27 | 3imtr4g 299 |
. . . . . . . . 9
⊢ (((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) ∧ 𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞)) → 𝑟 ∈ {𝑃})) |
29 | 28 | exp4b 434 |
. . . . . . . 8
⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → (𝑟 ∈ 𝐴 → ((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃})))) |
30 | 29 | com23 86 |
. . . . . . 7
⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → ((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) → (𝑟 ∈ 𝐴 → (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃})))) |
31 | 30 | ralrimdv 3110 |
. . . . . 6
⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → ((𝑝 ∈ {𝑃} ∧ 𝑞 ∈ {𝑃}) → ∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃}))) |
32 | 31 | ralrimivv 3112 |
. . . . 5
⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → ∀𝑝 ∈ {𝑃}∀𝑞 ∈ {𝑃}∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃})) |
33 | 2, 32 | jca 515 |
. . . 4
⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → ({𝑃} ⊆ 𝐴 ∧ ∀𝑝 ∈ {𝑃}∀𝑞 ∈ {𝑃}∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃}))) |
34 | 33 | ex 416 |
. . 3
⊢ (𝐾 ∈ AtLat → (𝑃 ∈ 𝐴 → ({𝑃} ⊆ 𝐴 ∧ ∀𝑝 ∈ {𝑃}∀𝑞 ∈ {𝑃}∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃})))) |
35 | | snpsub.s |
. . . 4
⊢ 𝑆 = (PSubSp‘𝐾) |
36 | 12, 7, 5, 35 | ispsubsp 37522 |
. . 3
⊢ (𝐾 ∈ AtLat → ({𝑃} ∈ 𝑆 ↔ ({𝑃} ⊆ 𝐴 ∧ ∀𝑝 ∈ {𝑃}∀𝑞 ∈ {𝑃}∀𝑟 ∈ 𝐴 (𝑟(le‘𝐾)(𝑝(join‘𝐾)𝑞) → 𝑟 ∈ {𝑃})))) |
37 | 34, 36 | sylibrd 262 |
. 2
⊢ (𝐾 ∈ AtLat → (𝑃 ∈ 𝐴 → {𝑃} ∈ 𝑆)) |
38 | 37 | imp 410 |
1
⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → {𝑃} ∈ 𝑆) |