Step | Hyp | Ref
| Expression |
1 | | df-rab 3411 |
. . . 4
β’ {π β π« π«
π β£ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))} = {π β£ (π β π« π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))} |
2 | | velpw 4570 |
. . . . . 6
β’ (π β π« π«
π β π β π« π) |
3 | 2 | anbi1i 625 |
. . . . 5
β’ ((π β π« π«
π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))) |
4 | 3 | abbii 2807 |
. . . 4
β’ {π β£ (π β π« π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))} = {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))} |
5 | 1, 4 | eqtri 2765 |
. . 3
β’ {π β π« π«
π β£ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))} = {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))} |
6 | | pwexg 5338 |
. . . 4
β’ (π β V β π« π β V) |
7 | | pwexg 5338 |
. . . 4
β’
(π« π β
V β π« π« π β V) |
8 | | rabexg 5293 |
. . . 4
β’
(π« π« π β V β {π β π« π« π β£ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))} β
V) |
9 | 6, 7, 8 | 3syl 18 |
. . 3
β’ (π β V β {π β π« π«
π β£ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))} β
V) |
10 | 5, 9 | eqeltrrid 2843 |
. 2
β’ (π β V β {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))} β
V) |
11 | | pweq 4579 |
. . . . . 6
β’ (π = π β π« π = π« π) |
12 | 11 | sseq2d 3981 |
. . . . 5
β’ (π = π β (π β π« π β π β π« π)) |
13 | | eleq1 2826 |
. . . . . 6
β’ (π = π β (π β π β π β π )) |
14 | | difeq1 4080 |
. . . . . . . 8
β’ (π = π β (π β π₯) = (π β π₯)) |
15 | 14 | eleq1d 2823 |
. . . . . . 7
β’ (π = π β ((π β π₯) β π β (π β π₯) β π )) |
16 | 15 | ralbidv 3175 |
. . . . . 6
β’ (π = π β (βπ₯ β π (π β π₯) β π β βπ₯ β π (π β π₯) β π )) |
17 | 13, 16 | 3anbi12d 1438 |
. . . . 5
β’ (π = π β ((π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )) β (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))) |
18 | 12, 17 | anbi12d 632 |
. . . 4
β’ (π = π β ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))))) |
19 | 18 | abbidv 2806 |
. . 3
β’ (π = π β {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))} = {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))}) |
20 | | df-siga 32748 |
. . 3
β’
sigAlgebra = (π
β V β¦ {π β£
(π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))}) |
21 | 19, 20 | fvmptg 6951 |
. 2
β’ ((π β V β§ {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))} β V)
β (sigAlgebraβπ)
= {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))}) |
22 | 10, 21 | mpdan 686 |
1
β’ (π β V β
(sigAlgebraβπ) =
{π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))}) |