Step |
Hyp |
Ref |
Expression |
1 |
|
df-sigagen |
⊢ sigaGen = ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 } ) |
2 |
1
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → sigaGen = ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 } ) ) |
3 |
|
unieq |
⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 ) |
4 |
3
|
fveq2d |
⊢ ( 𝑥 = 𝐴 → ( sigAlgebra ‘ ∪ 𝑥 ) = ( sigAlgebra ‘ ∪ 𝐴 ) ) |
5 |
|
sseq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝑠 ) ) |
6 |
4 5
|
rabeqbidv |
⊢ ( 𝑥 = 𝐴 → { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 } = { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ) |
7 |
6
|
inteqd |
⊢ ( 𝑥 = 𝐴 → ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 } = ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ) |
8 |
7
|
adantl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑥 = 𝐴 ) → ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝑥 ) ∣ 𝑥 ⊆ 𝑠 } = ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ) |
9 |
|
elex |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) |
10 |
|
uniexg |
⊢ ( 𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V ) |
11 |
|
pwsiga |
⊢ ( ∪ 𝐴 ∈ V → 𝒫 ∪ 𝐴 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ) |
12 |
10 11
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ) |
13 |
|
pwuni |
⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 |
14 |
12 13
|
jctir |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝒫 ∪ 𝐴 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴 ) ) |
15 |
|
sseq2 |
⊢ ( 𝑠 = 𝒫 ∪ 𝐴 → ( 𝐴 ⊆ 𝑠 ↔ 𝐴 ⊆ 𝒫 ∪ 𝐴 ) ) |
16 |
15
|
elrab |
⊢ ( 𝒫 ∪ 𝐴 ∈ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ↔ ( 𝒫 ∪ 𝐴 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∧ 𝐴 ⊆ 𝒫 ∪ 𝐴 ) ) |
17 |
14 16
|
sylibr |
⊢ ( 𝐴 ∈ 𝑉 → 𝒫 ∪ 𝐴 ∈ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ) |
18 |
17
|
ne0d |
⊢ ( 𝐴 ∈ 𝑉 → { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ≠ ∅ ) |
19 |
|
intex |
⊢ ( { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ≠ ∅ ↔ ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ∈ V ) |
20 |
18 19
|
sylib |
⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ∈ V ) |
21 |
2 8 9 20
|
fvmptd |
⊢ ( 𝐴 ∈ 𝑉 → ( sigaGen ‘ 𝐴 ) = ∩ { 𝑠 ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∣ 𝐴 ⊆ 𝑠 } ) |