Step | Hyp | Ref
| Expression |
1 | | df-sigagen 32778 |
. . 3
β’ sigaGen =
(π₯ β V β¦ β© {π
β (sigAlgebraββͺ π₯) β£ π₯ β π }) |
2 | 1 | a1i 11 |
. 2
β’ (π΄ β π β sigaGen = (π₯ β V β¦ β© {π
β (sigAlgebraββͺ π₯) β£ π₯ β π })) |
3 | | unieq 4881 |
. . . . . 6
β’ (π₯ = π΄ β βͺ π₯ = βͺ
π΄) |
4 | 3 | fveq2d 6851 |
. . . . 5
β’ (π₯ = π΄ β (sigAlgebraββͺ π₯) =
(sigAlgebraββͺ π΄)) |
5 | | sseq1 3974 |
. . . . 5
β’ (π₯ = π΄ β (π₯ β π β π΄ β π )) |
6 | 4, 5 | rabeqbidv 3427 |
. . . 4
β’ (π₯ = π΄ β {π β (sigAlgebraββͺ π₯)
β£ π₯ β π } = {π β (sigAlgebraββͺ π΄)
β£ π΄ β π }) |
7 | 6 | inteqd 4917 |
. . 3
β’ (π₯ = π΄ β β© {π β (sigAlgebraββͺ π₯)
β£ π₯ β π } = β©
{π β
(sigAlgebraββͺ π΄) β£ π΄ β π }) |
8 | 7 | adantl 483 |
. 2
β’ ((π΄ β π β§ π₯ = π΄) β β© {π β (sigAlgebraββͺ π₯)
β£ π₯ β π } = β©
{π β
(sigAlgebraββͺ π΄) β£ π΄ β π }) |
9 | | elex 3466 |
. 2
β’ (π΄ β π β π΄ β V) |
10 | | uniexg 7682 |
. . . . . . 7
β’ (π΄ β π β βͺ π΄ β V) |
11 | | pwsiga 32769 |
. . . . . . 7
β’ (βͺ π΄
β V β π« βͺ π΄ β (sigAlgebraββͺ π΄)) |
12 | 10, 11 | syl 17 |
. . . . . 6
β’ (π΄ β π β π« βͺ π΄
β (sigAlgebraββͺ π΄)) |
13 | | pwuni 4911 |
. . . . . 6
β’ π΄ β π« βͺ π΄ |
14 | 12, 13 | jctir 522 |
. . . . 5
β’ (π΄ β π β (π« βͺ π΄
β (sigAlgebraββͺ π΄) β§ π΄ β π« βͺ π΄)) |
15 | | sseq2 3975 |
. . . . . 6
β’ (π = π« βͺ π΄
β (π΄ β π β π΄ β π« βͺ π΄)) |
16 | 15 | elrab 3650 |
. . . . 5
β’
(π« βͺ π΄ β {π β (sigAlgebraββͺ π΄)
β£ π΄ β π } β (π« βͺ π΄
β (sigAlgebraββͺ π΄) β§ π΄ β π« βͺ π΄)) |
17 | 14, 16 | sylibr 233 |
. . . 4
β’ (π΄ β π β π« βͺ π΄
β {π β
(sigAlgebraββͺ π΄) β£ π΄ β π }) |
18 | 17 | ne0d 4300 |
. . 3
β’ (π΄ β π β {π β (sigAlgebraββͺ π΄)
β£ π΄ β π } β β
) |
19 | | intex 5299 |
. . 3
β’ ({π β (sigAlgebraββͺ π΄)
β£ π΄ β π } β β
β β© {π
β (sigAlgebraββͺ π΄) β£ π΄ β π } β V) |
20 | 18, 19 | sylib 217 |
. 2
β’ (π΄ β π β β© {π β (sigAlgebraββͺ π΄)
β£ π΄ β π } β V) |
21 | 2, 8, 9, 20 | fvmptd 6960 |
1
β’ (π΄ β π β (sigaGenβπ΄) = β© {π β (sigAlgebraββͺ π΄)
β£ π΄ β π }) |