Step | Hyp | Ref
| Expression |
1 | | elfvex 6885 |
. . . 4
β’ (π β (sigAlgebraβπ) β π β V) |
2 | | elex 3466 |
. . . 4
β’ (π β (sigAlgebraβπ) β π β V) |
3 | 1, 2 | jca 513 |
. . 3
β’ (π β (sigAlgebraβπ) β (π β V β§ π β V)) |
4 | 3 | a1i 11 |
. 2
β’ (π β V β (π β (sigAlgebraβπ) β (π β V β§ π β V))) |
5 | | simpr1 1195 |
. . . . 5
β’ ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β π β π) |
6 | | elex 3466 |
. . . . 5
β’ (π β π β π β V) |
7 | 5, 6 | syl 17 |
. . . 4
β’ ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β π β V) |
8 | 7 | a1i 11 |
. . 3
β’ (π β V β ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β π β V)) |
9 | 8 | anc2ri 558 |
. 2
β’ (π β V β ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β (π β V β§ π β V))) |
10 | | df-siga 32748 |
. . . 4
β’
sigAlgebra = (π
β V β¦ {π β£
(π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))}) |
11 | | sigaex 32749 |
. . . 4
β’ {π β£ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )))} β
V |
12 | | pweq 4579 |
. . . . . . 7
β’ (π = π β π« π = π« π) |
13 | 12 | sseq2d 3981 |
. . . . . 6
β’ (π = π β (π β π« π β π β π« π)) |
14 | | sseq1 3974 |
. . . . . 6
β’ (π = π β (π β π« π β π β π« π)) |
15 | 13, 14 | sylan9bb 511 |
. . . . 5
β’ ((π = π β§ π = π) β (π β π« π β π β π« π)) |
16 | | eleq12 2828 |
. . . . . 6
β’ ((π = π β§ π = π) β (π β π β π β π)) |
17 | | simpr 486 |
. . . . . . 7
β’ ((π = π β§ π = π) β π = π) |
18 | | difeq1 4080 |
. . . . . . . . . 10
β’ (π = π β (π β π₯) = (π β π₯)) |
19 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π = π β§ π = π) β (π β π₯) = (π β π₯)) |
20 | 19 | eleq1d 2823 |
. . . . . . . 8
β’ ((π = π β§ π = π) β ((π β π₯) β π β (π β π₯) β π )) |
21 | | eleq2 2827 |
. . . . . . . . 9
β’ (π = π β ((π β π₯) β π β (π β π₯) β π)) |
22 | 21 | adantl 483 |
. . . . . . . 8
β’ ((π = π β§ π = π) β ((π β π₯) β π β (π β π₯) β π)) |
23 | 20, 22 | bitrd 279 |
. . . . . . 7
β’ ((π = π β§ π = π) β ((π β π₯) β π β (π β π₯) β π)) |
24 | 17, 23 | raleqbidv 3322 |
. . . . . 6
β’ ((π = π β§ π = π) β (βπ₯ β π (π β π₯) β π β βπ₯ β π (π β π₯) β π)) |
25 | | pweq 4579 |
. . . . . . . 8
β’ (π = π β π« π = π« π) |
26 | | eleq2 2827 |
. . . . . . . . 9
β’ (π = π β (βͺ π₯ β π β βͺ π₯ β π)) |
27 | 26 | imbi2d 341 |
. . . . . . . 8
β’ (π = π β ((π₯ βΌ Ο β βͺ π₯
β π ) β (π₯ βΌ Ο β βͺ π₯
β π))) |
28 | 25, 27 | raleqbidv 3322 |
. . . . . . 7
β’ (π = π β (βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ) β
βπ₯ β π«
π(π₯ βΌ Ο β βͺ π₯
β π))) |
29 | 28 | adantl 483 |
. . . . . 6
β’ ((π = π β§ π = π) β (βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ) β
βπ₯ β π«
π(π₯ βΌ Ο β βͺ π₯
β π))) |
30 | 16, 24, 29 | 3anbi123d 1437 |
. . . . 5
β’ ((π = π β§ π = π) β ((π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π )) β (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) |
31 | 15, 30 | anbi12d 632 |
. . . 4
β’ ((π = π β§ π = π) β ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π (π₯ βΌ Ο β βͺ π₯
β π ))) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))))) |
32 | 10, 11, 31 | abfmpel 31613 |
. . 3
β’ ((π β V β§ π β V) β (π β (sigAlgebraβπ) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))))) |
33 | 32 | a1i 11 |
. 2
β’ (π β V β ((π β V β§ π β V) β (π β (sigAlgebraβπ) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))))) |
34 | 4, 9, 33 | pm5.21ndd 381 |
1
β’ (π β V β (π β (sigAlgebraβπ) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))))) |