Step | Hyp | Ref
| Expression |
1 | | elex 3364 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | simpr 471 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩
𝑥) → 𝑦 = ∩
𝑥) |
3 | | inss1 3982 |
. . . . . . . . . 10
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 |
4 | 3 | sseli 3749 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) |
5 | 4 | elpwid 4310 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴) |
6 | | eqvisset 3363 |
. . . . . . . . 9
⊢ (𝑦 = ∩
𝑥 → ∩ 𝑥
∈ V) |
7 | | intex 4952 |
. . . . . . . . 9
⊢ (𝑥 ≠ ∅ ↔ ∩ 𝑥
∈ V) |
8 | 6, 7 | sylibr 224 |
. . . . . . . 8
⊢ (𝑦 = ∩
𝑥 → 𝑥 ≠ ∅) |
9 | | intssuni2 4637 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∩ 𝑥
⊆ ∪ 𝐴) |
10 | 5, 8, 9 | syl2an 577 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩
𝑥) → ∩ 𝑥
⊆ ∪ 𝐴) |
11 | 2, 10 | eqsstrd 3789 |
. . . . . 6
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩
𝑥) → 𝑦 ⊆ ∪ 𝐴) |
12 | | selpw 4305 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 ∪ 𝐴
↔ 𝑦 ⊆ ∪ 𝐴) |
13 | 11, 12 | sylibr 224 |
. . . . 5
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩
𝑥) → 𝑦 ∈ 𝒫 ∪ 𝐴) |
14 | 13 | rexlimiva 3176 |
. . . 4
⊢
(∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)𝑦 = ∩ 𝑥
→ 𝑦 ∈ 𝒫
∪ 𝐴) |
15 | 14 | abssi 3827 |
. . 3
⊢ {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ⊆ 𝒫 ∪ 𝐴 |
16 | | uniexg 7103 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
17 | | pwexg 4981 |
. . . 4
⊢ (∪ 𝐴
∈ V → 𝒫 ∪ 𝐴 ∈ V) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴
∈ V) |
19 | | ssexg 4939 |
. . 3
⊢ (({𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ⊆ 𝒫 ∪ 𝐴
∧ 𝒫 ∪ 𝐴 ∈ V) → {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ∈ V) |
20 | 15, 18, 19 | sylancr 569 |
. 2
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ∈ V) |
21 | | pweq 4301 |
. . . . . 6
⊢ (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴) |
22 | 21 | ineq1d 3965 |
. . . . 5
⊢ (𝑧 = 𝐴 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝐴 ∩ Fin)) |
23 | 22 | rexeqdv 3294 |
. . . 4
⊢ (𝑧 = 𝐴 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑦 = ∩ 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥)) |
24 | 23 | abbidv 2890 |
. . 3
⊢ (𝑧 = 𝐴 → {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑦 = ∩ 𝑥} = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) |
25 | | df-fi 8474 |
. . 3
⊢ fi =
(𝑧 ∈ V ↦ {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑦 = ∩ 𝑥}) |
26 | 24, 25 | fvmptg 6423 |
. 2
⊢ ((𝐴 ∈ V ∧ {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ∈ V) →
(fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) |
27 | 1, 20, 26 | syl2anc 567 |
1
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) |