Step | Hyp | Ref
| Expression |
1 | | pclfval.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
2 | | fvex 6201 |
. . . 4
⊢
(Atoms‘𝐾)
∈ V |
3 | 1, 2 | eqeltri 2697 |
. . 3
⊢ 𝐴 ∈ V |
4 | 3 | elpw2 4828 |
. 2
⊢ (𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴) |
5 | | pclfval.s |
. . . . . 6
⊢ 𝑆 = (PSubSp‘𝐾) |
6 | | pclfval.c |
. . . . . 6
⊢ 𝑈 = (PCl‘𝐾) |
7 | 1, 5, 6 | pclfvalN 35175 |
. . . . 5
⊢ (𝐾 ∈ 𝑉 → 𝑈 = (𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦})) |
8 | 7 | fveq1d 6193 |
. . . 4
⊢ (𝐾 ∈ 𝑉 → (𝑈‘𝑋) = ((𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦})‘𝑋)) |
9 | 8 | adantr 481 |
. . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → (𝑈‘𝑋) = ((𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦})‘𝑋)) |
10 | | simpr 477 |
. . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → 𝑋 ∈ 𝒫 𝐴) |
11 | | elpwi 4168 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝒫 𝐴 → 𝑋 ⊆ 𝐴) |
12 | 11 | adantl 482 |
. . . . . . 7
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → 𝑋 ⊆ 𝐴) |
13 | 1, 5 | atpsubN 35039 |
. . . . . . . . 9
⊢ (𝐾 ∈ 𝑉 → 𝐴 ∈ 𝑆) |
14 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → 𝐴 ∈ 𝑆) |
15 | | sseq2 3627 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → (𝑋 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝐴)) |
16 | 15 | elrab3 3364 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑆 → (𝐴 ∈ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦} ↔ 𝑋 ⊆ 𝐴)) |
17 | 14, 16 | syl 17 |
. . . . . . 7
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → (𝐴 ∈ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦} ↔ 𝑋 ⊆ 𝐴)) |
18 | 12, 17 | mpbird 247 |
. . . . . 6
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → 𝐴 ∈ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦}) |
19 | | ne0i 3921 |
. . . . . 6
⊢ (𝐴 ∈ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦} → {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦} ≠ ∅) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦} ≠ ∅) |
21 | | intex 4820 |
. . . . 5
⊢ ({𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦} ≠ ∅ ↔ ∩ {𝑦
∈ 𝑆 ∣ 𝑋 ⊆ 𝑦} ∈ V) |
22 | 20, 21 | sylib 208 |
. . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦} ∈ V) |
23 | | sseq1 3626 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝑦)) |
24 | 23 | rabbidv 3189 |
. . . . . 6
⊢ (𝑥 = 𝑋 → {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦} = {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦}) |
25 | 24 | inteqd 4480 |
. . . . 5
⊢ (𝑥 = 𝑋 → ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦} = ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦}) |
26 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦
∈ 𝑆 ∣ 𝑥 ⊆ 𝑦}) = (𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦}) |
27 | 25, 26 | fvmptg 6280 |
. . . 4
⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ ∩ {𝑦
∈ 𝑆 ∣ 𝑋 ⊆ 𝑦} ∈ V) → ((𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦})‘𝑋) = ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦}) |
28 | 10, 22, 27 | syl2anc 693 |
. . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦})‘𝑋) = ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦}) |
29 | 9, 28 | eqtrd 2656 |
. 2
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝒫 𝐴) → (𝑈‘𝑋) = ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦}) |
30 | 4, 29 | sylan2br 493 |
1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦}) |