Proof of Theorem pmapglb2N
Step | Hyp | Ref
| Expression |
1 | | hlop 34649 |
. . . . 5
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
2 | | pmapglb2.g |
. . . . . . . 8
⊢ 𝐺 = (glb‘𝐾) |
3 | | eqid 2622 |
. . . . . . . 8
⊢
(1.‘𝐾) =
(1.‘𝐾) |
4 | 2, 3 | glb0N 34480 |
. . . . . . 7
⊢ (𝐾 ∈ OP → (𝐺‘∅) =
(1.‘𝐾)) |
5 | 4 | fveq2d 6195 |
. . . . . 6
⊢ (𝐾 ∈ OP → (𝑀‘(𝐺‘∅)) = (𝑀‘(1.‘𝐾))) |
6 | | pmapglb2.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
7 | | pmapglb2.m |
. . . . . . 7
⊢ 𝑀 = (pmap‘𝐾) |
8 | 3, 6, 7 | pmap1N 35053 |
. . . . . 6
⊢ (𝐾 ∈ OP → (𝑀‘(1.‘𝐾)) = 𝐴) |
9 | 5, 8 | eqtrd 2656 |
. . . . 5
⊢ (𝐾 ∈ OP → (𝑀‘(𝐺‘∅)) = 𝐴) |
10 | 1, 9 | syl 17 |
. . . 4
⊢ (𝐾 ∈ HL → (𝑀‘(𝐺‘∅)) = 𝐴) |
11 | | fveq2 6191 |
. . . . . 6
⊢ (𝑆 = ∅ → (𝐺‘𝑆) = (𝐺‘∅)) |
12 | 11 | fveq2d 6195 |
. . . . 5
⊢ (𝑆 = ∅ → (𝑀‘(𝐺‘𝑆)) = (𝑀‘(𝐺‘∅))) |
13 | | riin0 4594 |
. . . . 5
⊢ (𝑆 = ∅ → (𝐴 ∩ ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥)) = 𝐴) |
14 | 12, 13 | eqeq12d 2637 |
. . . 4
⊢ (𝑆 = ∅ → ((𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) ↔ (𝑀‘(𝐺‘∅)) = 𝐴)) |
15 | 10, 14 | syl5ibrcom 237 |
. . 3
⊢ (𝐾 ∈ HL → (𝑆 = ∅ → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)))) |
16 | 15 | adantr 481 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑆 = ∅ → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)))) |
17 | | pmapglb2.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
18 | 17, 2, 7 | pmapglb 35056 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝑀‘(𝐺‘𝑆)) = ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) |
19 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
20 | | simpll 790 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝐾 ∈ HL) |
21 | | ssel2 3598 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
22 | 21 | adantll 750 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
23 | 17, 6, 7 | pmapssat 35045 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑥 ∈ 𝐵) → (𝑀‘𝑥) ⊆ 𝐴) |
24 | 20, 22, 23 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑀‘𝑥) ⊆ 𝐴) |
25 | 19, 24 | jca 554 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴)) |
26 | 25 | ex 450 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑥 ∈ 𝑆 → (𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴))) |
27 | 26 | eximdv 1846 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (∃𝑥 𝑥 ∈ 𝑆 → ∃𝑥(𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴))) |
28 | | n0 3931 |
. . . . . . . 8
⊢ (𝑆 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝑆) |
29 | | df-rex 2918 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑆 (𝑀‘𝑥) ⊆ 𝐴 ↔ ∃𝑥(𝑥 ∈ 𝑆 ∧ (𝑀‘𝑥) ⊆ 𝐴)) |
30 | 27, 28, 29 | 3imtr4g 285 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑆 ≠ ∅ → ∃𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴)) |
31 | 30 | 3impia 1261 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → ∃𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴) |
32 | | iinss 4571 |
. . . . . 6
⊢
(∃𝑥 ∈
𝑆 (𝑀‘𝑥) ⊆ 𝐴 → ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴) |
34 | | sseqin2 3817 |
. . . . 5
⊢ (∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥) ⊆ 𝐴 ↔ (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) = ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) |
35 | 33, 34 | sylib 208 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) = ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)) |
36 | 18, 35 | eqtr4d 2659 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥))) |
37 | 36 | 3expia 1267 |
. 2
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑆 ≠ ∅ → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥)))) |
38 | 16, 37 | pm2.61dne 2880 |
1
⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩
𝑥 ∈ 𝑆 (𝑀‘𝑥))) |