Proof of Theorem pmapglb2N
Step | Hyp | Ref
| Expression |
1 | | hlop 33667 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
2 | | pmapglb2.g |
. . . . . . . 8
⊢ 𝐺 = (glb‘𝐾) |
3 | | eqid 2610 |
. . . . . . . 8
⊢
(1.‘𝐾) =
(1.‘𝐾) |
4 | 2, 3 | glb0N 33498 |
. . . . . . 7
⊢ (𝐾 ∈ OP → (𝐺‘∅) =
(1.‘𝐾)) |
5 | 4 | fveq2d 6107 |
. . . . . 6
⊢ (𝐾 ∈ OP → (𝑀‘(𝐺‘∅)) = (𝑀‘(1.‘𝐾))) |
6 | | pmapglb2.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
7 | | pmapglb2.m |
. . . . . . 7
⊢ 𝑀 = (pmap‘𝐾) |
8 | 3, 6, 7 | pmap1N 34071 |
. . . . . 6
⊢ (𝐾 ∈ OP → (𝑀‘(1.‘𝐾)) = 𝐴) |
9 | 5, 8 | eqtrd 2644 |
. . . . 5
⊢ (𝐾 ∈ OP → (𝑀‘(𝐺‘∅)) = 𝐴) |
10 | 1, 9 | syl 17 |
. . . 4
⊢ (𝐾 ∈ HL → (𝑀‘(𝐺‘∅)) = 𝐴) |
11 | | fveq2 6103 |
. . . . . 6
⊢ (𝑆 = ∅ → (𝐺‘𝑆) = (𝐺‘∅)) |
12 | 11 | fveq2d 6107 |
. . . . 5
⊢ (𝑆 = ∅ → (𝑀‘(𝐺‘𝑆)) = (𝑀‘(𝐺‘∅))) |
13 | | riin0 4530 |
. . . . 5
⊢ (𝑆 = ∅ → (𝐴 ∩ ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥)) = 𝐴) |
14 | 12, 13 | eqeq12d 2625 |
. . . 4
⊢ (𝑆 = ∅ → ((𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) ↔ (𝑀‘(𝐺‘∅)) = 𝐴)) |
15 | 10, 14 | syl5ibrcom 236 |
. . 3
⊢ (𝐾 ∈ HL → (𝑆 = ∅ → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)))) |
16 | 15 | adantr 480 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑆 = ∅ → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)))) |
17 | | pmapglb2.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
18 | 17, 2, 7 | pmapglb 34074 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝑀‘(𝐺‘𝑆)) = ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) |
19 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
20 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ HL) |
21 | | ssel2 3563 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
22 | 21 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
23 | 17, 6, 7 | pmapssat 34063 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑥 ∈ 𝐵) → (𝑀‘𝑥) ⊆ 𝐴) |
24 | 20, 22, 23 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑀‘𝑥) ⊆ 𝐴) |
25 | 19, 24 | jca 553 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴)) |
26 | 25 | ex 449 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴))) |
27 | 26 | eximdv 1833 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴))) |
28 | | n0 3890 |
. . . . . . . 8
⊢ (𝑆 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑆) |
29 | | df-rex 2902 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑆 (𝑀‘𝑥) ⊆ 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴)) |
30 | 27, 28, 29 | 3imtr4g 284 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑆 ≠ ∅ → ∃𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴)) |
31 | 30 | 3impia 1253 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → ∃𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴) |
32 | | iinss 4507 |
. . . . . 6
⊢
(∃𝑥 ∈
𝑆 (𝑀‘𝑥) ⊆ 𝐴 → ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴) |
34 | | sseqin2 3779 |
. . . . 5
⊢ (∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴 ↔ (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) = ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) |
35 | 33, 34 | sylib 207 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) = ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) |
36 | 18, 35 | eqtr4d 2647 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥))) |
37 | 36 | 3expia 1259 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑆 ≠ ∅ → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)))) |
38 | 16, 37 | pm2.61dne 2868 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥))) |