Step | Hyp | Ref
| Expression |
1 | | df-sigagen 30202 |
. . 3
⊢ sigaGen =
(𝑥 ∈ V ↦ ∩ {𝑠
∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠}) |
2 | 1 | a1i 11 |
. 2
⊢ (𝐴 ∈ 𝑉 → sigaGen = (𝑥 ∈ V ↦ ∩ {𝑠
∈ (sigAlgebra‘∪ 𝑥) ∣ 𝑥 ⊆ 𝑠})) |
3 | | unieq 4444 |
. . . . . 6
⊢ (𝑥 = 𝐴 → ∪ 𝑥 = ∪
𝐴) |
4 | 3 | fveq2d 6195 |
. . . . 5
⊢ (𝑥 = 𝐴 → (sigAlgebra‘∪ 𝑥) =
(sigAlgebra‘∪ 𝐴)) |
5 | | sseq1 3626 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝑥 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠)) |
6 | 4, 5 | rabeqbidv 3195 |
. . . 4
⊢ (𝑥 = 𝐴 → {𝑠 ∈ (sigAlgebra‘∪ 𝑥)
∣ 𝑥 ⊆ 𝑠} = {𝑠 ∈ (sigAlgebra‘∪ 𝐴)
∣ 𝐴 ⊆ 𝑠}) |
7 | 6 | inteqd 4480 |
. . 3
⊢ (𝑥 = 𝐴 → ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥)
∣ 𝑥 ⊆ 𝑠} = ∩
{𝑠 ∈
(sigAlgebra‘∪ 𝐴) ∣ 𝐴 ⊆ 𝑠}) |
8 | 7 | adantl 482 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 = 𝐴) → ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝑥)
∣ 𝑥 ⊆ 𝑠} = ∩
{𝑠 ∈
(sigAlgebra‘∪ 𝐴) ∣ 𝐴 ⊆ 𝑠}) |
9 | | elex 3212 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
10 | | uniexg 6955 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V) |
11 | | pwsiga 30193 |
. . . . . . 7
⊢ (∪ 𝐴
∈ V → 𝒫 ∪ 𝐴 ∈ (sigAlgebra‘∪ 𝐴)) |
12 | 10, 11 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴
∈ (sigAlgebra‘∪ 𝐴)) |
13 | | pwuni 4474 |
. . . . . 6
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 |
14 | 12, 13 | jctir 561 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝒫 ∪ 𝐴
∈ (sigAlgebra‘∪ 𝐴) ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴)) |
15 | | sseq2 3627 |
. . . . . 6
⊢ (𝑠 = 𝒫 ∪ 𝐴
→ (𝐴 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝒫 ∪ 𝐴)) |
16 | 15 | elrab 3363 |
. . . . 5
⊢
(𝒫 ∪ 𝐴 ∈ {𝑠 ∈ (sigAlgebra‘∪ 𝐴)
∣ 𝐴 ⊆ 𝑠} ↔ (𝒫 ∪ 𝐴
∈ (sigAlgebra‘∪ 𝐴) ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴)) |
17 | 14, 16 | sylibr 224 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴
∈ {𝑠 ∈
(sigAlgebra‘∪ 𝐴) ∣ 𝐴 ⊆ 𝑠}) |
18 | | ne0i 3921 |
. . . 4
⊢
(𝒫 ∪ 𝐴 ∈ {𝑠 ∈ (sigAlgebra‘∪ 𝐴)
∣ 𝐴 ⊆ 𝑠} → {𝑠 ∈ (sigAlgebra‘∪ 𝐴)
∣ 𝐴 ⊆ 𝑠} ≠ ∅) |
19 | 17, 18 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → {𝑠 ∈ (sigAlgebra‘∪ 𝐴)
∣ 𝐴 ⊆ 𝑠} ≠ ∅) |
20 | | intex 4820 |
. . 3
⊢ ({𝑠 ∈ (sigAlgebra‘∪ 𝐴)
∣ 𝐴 ⊆ 𝑠} ≠ ∅ ↔ ∩ {𝑠
∈ (sigAlgebra‘∪ 𝐴) ∣ 𝐴 ⊆ 𝑠} ∈ V) |
21 | 19, 20 | sylib 208 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝐴)
∣ 𝐴 ⊆ 𝑠} ∈ V) |
22 | 2, 8, 9, 21 | fvmptd 6288 |
1
⊢ (𝐴 ∈ 𝑉 → (sigaGen‘𝐴) = ∩ {𝑠 ∈ (sigAlgebra‘∪ 𝐴)
∣ 𝐴 ⊆ 𝑠}) |