Proof of Theorem pmapglb2xN
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 | | rexeq 3116 |
. . . . . . . . 9
⊢ (𝐼 = ∅ → (∃𝑖 ∈ 𝐼 𝑦 = 𝑆 ↔ ∃𝑖 ∈ ∅ 𝑦 = 𝑆)) |
12 | 11 | abbidv 2728 |
. . . . . . . 8
⊢ (𝐼 = ∅ → {𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆} = {𝑦 ∣ ∃𝑖 ∈ ∅ 𝑦 = 𝑆}) |
13 | | rex0 3894 |
. . . . . . . . 9
⊢ ¬
∃𝑖 ∈ ∅
𝑦 = 𝑆 |
14 | 13 | abf 3930 |
. . . . . . . 8
⊢ {𝑦 ∣ ∃𝑖 ∈ ∅ 𝑦 = 𝑆} = ∅ |
15 | 12, 14 | syl6eq 2660 |
. . . . . . 7
⊢ (𝐼 = ∅ → {𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆} = ∅) |
16 | 15 | fveq2d 6107 |
. . . . . 6
⊢ (𝐼 = ∅ → (𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆}) = (𝐺‘∅)) |
17 | 16 | fveq2d 6107 |
. . . . 5
⊢ (𝐼 = ∅ → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = (𝑀‘(𝐺‘∅))) |
18 | | riin0 4530 |
. . . . 5
⊢ (𝐼 = ∅ → (𝐴 ∩ ∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆)) = 𝐴) |
19 | 17, 18 | eqeq12d 2625 |
. . . 4
⊢ (𝐼 = ∅ → ((𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = (𝐴 ∩ ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆)) ↔ (𝑀‘(𝐺‘∅)) = 𝐴)) |
20 | 10, 19 | syl5ibrcom 236 |
. . 3
⊢ (𝐾 ∈ HL → (𝐼 = ∅ → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = (𝐴 ∩ ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆)))) |
21 | 20 | adantr 480 |
. 2
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝐼 = ∅ → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = (𝐴 ∩ ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆)))) |
22 | | pmapglb2.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
23 | 22, 2, 7 | pmapglbx 34073 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆)) |
24 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑖 𝐾 ∈ HL |
25 | | nfra1 2925 |
. . . . . . . . . 10
⊢
Ⅎ𝑖∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 |
26 | 24, 25 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) |
27 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼) |
28 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) → 𝐾 ∈ HL) |
29 | | rspa 2914 |
. . . . . . . . . . . . 13
⊢
((∀𝑖 ∈
𝐼 𝑆 ∈ 𝐵 ∧ 𝑖 ∈ 𝐼) → 𝑆 ∈ 𝐵) |
30 | 29 | adantll 746 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) → 𝑆 ∈ 𝐵) |
31 | 22, 6, 7 | pmapssat 34063 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑆 ∈ 𝐵) → (𝑀‘𝑆) ⊆ 𝐴) |
32 | 28, 30, 31 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) → (𝑀‘𝑆) ⊆ 𝐴) |
33 | 27, 32 | jca 553 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) ∧ 𝑖 ∈ 𝐼) → (𝑖 ∈ 𝐼 ∧ (𝑀‘𝑆) ⊆ 𝐴)) |
34 | 33 | ex 449 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝑖 ∈ 𝐼 → (𝑖 ∈ 𝐼 ∧ (𝑀‘𝑆) ⊆ 𝐴))) |
35 | 26, 34 | eximd 2072 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (∃𝑖 𝑖 ∈ 𝐼 → ∃𝑖(𝑖 ∈ 𝐼 ∧ (𝑀‘𝑆) ⊆ 𝐴))) |
36 | | n0 3890 |
. . . . . . . 8
⊢ (𝐼 ≠ ∅ ↔
∃𝑖 𝑖 ∈ 𝐼) |
37 | | df-rex 2902 |
. . . . . . . 8
⊢
(∃𝑖 ∈
𝐼 (𝑀‘𝑆) ⊆ 𝐴 ↔ ∃𝑖(𝑖 ∈ 𝐼 ∧ (𝑀‘𝑆) ⊆ 𝐴)) |
38 | 35, 36, 37 | 3imtr4g 284 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝐼 ≠ ∅ → ∃𝑖 ∈ 𝐼 (𝑀‘𝑆) ⊆ 𝐴)) |
39 | 38 | 3impia 1253 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → ∃𝑖 ∈ 𝐼 (𝑀‘𝑆) ⊆ 𝐴) |
40 | | iinss 4507 |
. . . . . 6
⊢
(∃𝑖 ∈
𝐼 (𝑀‘𝑆) ⊆ 𝐴 → ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆) ⊆ 𝐴) |
41 | 39, 40 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → ∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆) ⊆ 𝐴) |
42 | | sseqin2 3779 |
. . . . 5
⊢ (∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆) ⊆ 𝐴 ↔ (𝐴 ∩ ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆)) = ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆)) |
43 | 41, 42 | sylib 207 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → (𝐴 ∩ ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆)) = ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆)) |
44 | 23, 43 | eqtr4d 2647 |
. . 3
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = (𝐴 ∩ ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆))) |
45 | 44 | 3expia 1259 |
. 2
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝐼 ≠ ∅ → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = (𝐴 ∩ ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆)))) |
46 | 21, 45 | pm2.61dne 2868 |
1
⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = (𝐴 ∩ ∩
𝑖 ∈ 𝐼 (𝑀‘𝑆))) |