Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
2 | | simpr 476 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩
𝑥) → 𝑦 = ∩
𝑥) |
3 | | inss1 3795 |
. . . . . . . . . 10
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 |
4 | 3 | sseli 3564 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) |
5 | 4 | elpwid 4118 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴) |
6 | | eqvisset 3184 |
. . . . . . . . 9
⊢ (𝑦 = ∩
𝑥 → ∩ 𝑥
∈ V) |
7 | | intex 4747 |
. . . . . . . . 9
⊢ (𝑥 ≠ ∅ ↔ ∩ 𝑥
∈ V) |
8 | 6, 7 | sylibr 223 |
. . . . . . . 8
⊢ (𝑦 = ∩
𝑥 → 𝑥 ≠ ∅) |
9 | | intssuni2 4437 |
. . . . . . . 8
⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∩ 𝑥
⊆ ∪ 𝐴) |
10 | 5, 8, 9 | syl2an 493 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩
𝑥) → ∩ 𝑥
⊆ ∪ 𝐴) |
11 | 2, 10 | eqsstrd 3602 |
. . . . . 6
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩
𝑥) → 𝑦 ⊆ ∪ 𝐴) |
12 | | selpw 4115 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 ∪ 𝐴
↔ 𝑦 ⊆ ∪ 𝐴) |
13 | 11, 12 | sylibr 223 |
. . . . 5
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑦 = ∩
𝑥) → 𝑦 ∈ 𝒫 ∪ 𝐴) |
14 | 13 | rexlimiva 3010 |
. . . 4
⊢
(∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)𝑦 = ∩ 𝑥
→ 𝑦 ∈ 𝒫
∪ 𝐴) |
15 | 14 | abssi 3640 |
. . 3
⊢ {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ⊆ 𝒫 ∪ 𝐴 |
16 | | uniexg 6853 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
17 | | pwexg 4776 |
. . . 4
⊢ (∪ 𝐴
∈ V → 𝒫 ∪ 𝐴 ∈ V) |
18 | 16, 17 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴
∈ V) |
19 | | ssexg 4732 |
. . 3
⊢ (({𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ⊆ 𝒫 ∪ 𝐴
∧ 𝒫 ∪ 𝐴 ∈ V) → {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ∈ V) |
20 | 15, 18, 19 | sylancr 694 |
. 2
⊢ (𝐴 ∈ 𝑉 → {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ∈ V) |
21 | | pweq 4111 |
. . . . . 6
⊢ (𝑧 = 𝐴 → 𝒫 𝑧 = 𝒫 𝐴) |
22 | 21 | ineq1d 3775 |
. . . . 5
⊢ (𝑧 = 𝐴 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝐴 ∩ Fin)) |
23 | 22 | rexeqdv 3122 |
. . . 4
⊢ (𝑧 = 𝐴 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑦 = ∩ 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥)) |
24 | 23 | abbidv 2728 |
. . 3
⊢ (𝑧 = 𝐴 → {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑦 = ∩ 𝑥} = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) |
25 | | df-fi 8200 |
. . 3
⊢ fi =
(𝑧 ∈ V ↦ {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑦 = ∩ 𝑥}) |
26 | 24, 25 | fvmptg 6189 |
. 2
⊢ ((𝐴 ∈ V ∧ {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥} ∈ V) →
(fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) |
27 | 1, 20, 26 | syl2anc 691 |
1
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = {𝑦 ∣ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑦 = ∩ 𝑥}) |