Step | Hyp | Ref
| Expression |
1 | | fvssunirn 6880 |
. . . 4
β’
(sigAlgebraβπ)
β βͺ ran sigAlgebra |
2 | 1 | sseli 3945 |
. . 3
β’ (π β (sigAlgebraβπ) β π β βͺ ran
sigAlgebra) |
3 | | elex 3466 |
. . . 4
β’ (π β (sigAlgebraβπ) β π β V) |
4 | | issiga 32751 |
. . . . 5
β’ (π β V β (π β (sigAlgebraβπ) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))))) |
5 | | elpwuni 5070 |
. . . . . . . 8
β’ (π β π β (π β π« π β βͺ π = π)) |
6 | 5 | biimpa 478 |
. . . . . . 7
β’ ((π β π β§ π β π« π) β βͺ π = π) |
7 | | ancom 462 |
. . . . . . 7
β’ ((π β π« π β§ π β π) β (π β π β§ π β π« π)) |
8 | | eqcom 2744 |
. . . . . . 7
β’ (π = βͺ
π β βͺ π =
π) |
9 | 6, 7, 8 | 3imtr4i 292 |
. . . . . 6
β’ ((π β π« π β§ π β π) β π = βͺ π) |
10 | 9 | 3ad2antr1 1189 |
. . . . 5
β’ ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β π = βͺ
π) |
11 | 4, 10 | syl6bi 253 |
. . . 4
β’ (π β V β (π β (sigAlgebraβπ) β π = βͺ π)) |
12 | 3, 11 | mpcom 38 |
. . 3
β’ (π β (sigAlgebraβπ) β π = βͺ π) |
13 | 2, 12 | jca 513 |
. 2
β’ (π β (sigAlgebraβπ) β (π β βͺ ran
sigAlgebra β§ π = βͺ π)) |
14 | | elex 3466 |
. . . . 5
β’ (π β βͺ ran sigAlgebra β π β V) |
15 | | isrnsiga 32752 |
. . . . . . . 8
β’ (π β βͺ ran sigAlgebra β (π β V β§ βπ(π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))))) |
16 | 15 | simprbi 498 |
. . . . . . 7
β’ (π β βͺ ran sigAlgebra β βπ(π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) |
17 | | elpwuni 5070 |
. . . . . . . . . . . . 13
β’ (π β π β (π β π« π β βͺ π = π)) |
18 | 17 | biimpa 478 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π« π) β βͺ π = π) |
19 | | ancom 462 |
. . . . . . . . . . . 12
β’ ((π β π« π β§ π β π) β (π β π β§ π β π« π)) |
20 | | eqcom 2744 |
. . . . . . . . . . . 12
β’ (π = βͺ
π β βͺ π =
π) |
21 | 18, 19, 20 | 3imtr4i 292 |
. . . . . . . . . . 11
β’ ((π β π« π β§ π β π) β π = βͺ π) |
22 | 21 | 3ad2antr1 1189 |
. . . . . . . . . 10
β’ ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β π = βͺ
π) |
23 | | pweq 4579 |
. . . . . . . . . . . 12
β’ (π = βͺ
π β π« π = π« βͺ π) |
24 | 23 | sseq2d 3981 |
. . . . . . . . . . 11
β’ (π = βͺ
π β (π β π« π β π β π« βͺ π)) |
25 | | eleq1 2826 |
. . . . . . . . . . . 12
β’ (π = βͺ
π β (π β π β βͺ π β π)) |
26 | | difeq1 4080 |
. . . . . . . . . . . . . 14
β’ (π = βͺ
π β (π β π₯) = (βͺ π β π₯)) |
27 | 26 | eleq1d 2823 |
. . . . . . . . . . . . 13
β’ (π = βͺ
π β ((π β π₯) β π β (βͺ π β π₯) β π)) |
28 | 27 | ralbidv 3175 |
. . . . . . . . . . . 12
β’ (π = βͺ
π β (βπ₯ β π (π β π₯) β π β βπ₯ β π (βͺ π β π₯) β π)) |
29 | 25, 28 | 3anbi12d 1438 |
. . . . . . . . . . 11
β’ (π = βͺ
π β ((π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)) β (βͺ π
β π β§
βπ₯ β π (βͺ
π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) |
30 | 24, 29 | anbi12d 632 |
. . . . . . . . . 10
β’ (π = βͺ
π β ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β (π β π« βͺ π
β§ (βͺ π β π β§ βπ₯ β π (βͺ π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))))) |
31 | 22, 30 | syl 17 |
. . . . . . . . 9
β’ ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β (π β π« βͺ π
β§ (βͺ π β π β§ βπ₯ β π (βͺ π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))))) |
32 | 31 | ibi 267 |
. . . . . . . 8
β’ ((π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β (π β π« βͺ π
β§ (βͺ π β π β§ βπ₯ β π (βͺ π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) |
33 | 32 | exlimiv 1934 |
. . . . . . 7
β’
(βπ(π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β (π β π« βͺ π
β§ (βͺ π β π β§ βπ₯ β π (βͺ π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) |
34 | 16, 33 | syl 17 |
. . . . . 6
β’ (π β βͺ ran sigAlgebra β (π β π« βͺ π
β§ (βͺ π β π β§ βπ₯ β π (βͺ π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) |
35 | 34 | simprd 497 |
. . . . 5
β’ (π β βͺ ran sigAlgebra β (βͺ
π β π β§ βπ₯ β π (βͺ π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) |
36 | 14, 35 | jca 513 |
. . . 4
β’ (π β βͺ ran sigAlgebra β (π β V β§ (βͺ π
β π β§
βπ₯ β π (βͺ
π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) |
37 | | eleq1 2826 |
. . . . . . . 8
β’ (π = βͺ
π β (π β π β βͺ π β π)) |
38 | | difeq1 4080 |
. . . . . . . . . 10
β’ (π = βͺ
π β (π β π₯) = (βͺ π β π₯)) |
39 | 38 | eleq1d 2823 |
. . . . . . . . 9
β’ (π = βͺ
π β ((π β π₯) β π β (βͺ π β π₯) β π)) |
40 | 39 | ralbidv 3175 |
. . . . . . . 8
β’ (π = βͺ
π β (βπ₯ β π (π β π₯) β π β βπ₯ β π (βͺ π β π₯) β π)) |
41 | 37, 40 | 3anbi12d 1438 |
. . . . . . 7
β’ (π = βͺ
π β ((π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)) β (βͺ π
β π β§
βπ₯ β π (βͺ
π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) |
42 | 41 | biimprd 248 |
. . . . . 6
β’ (π = βͺ
π β ((βͺ π
β π β§
βπ₯ β π (βͺ
π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)) β (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) |
43 | | pwuni 4911 |
. . . . . . 7
β’ π β π« βͺ π |
44 | | pweq 4579 |
. . . . . . 7
β’ (π = βͺ
π β π« π = π« βͺ π) |
45 | 43, 44 | sseqtrrid 4002 |
. . . . . 6
β’ (π = βͺ
π β π β π« π) |
46 | 42, 45 | jctild 527 |
. . . . 5
β’ (π = βͺ
π β ((βͺ π
β π β§
βπ₯ β π (βͺ
π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)) β (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))))) |
47 | 46 | anim2d 613 |
. . . 4
β’ (π = βͺ
π β ((π β V β§ (βͺ π
β π β§
βπ₯ β π (βͺ
π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π))) β (π β V β§ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))))) |
48 | 4 | biimpar 479 |
. . . 4
β’ ((π β V β§ (π β π« π β§ (π β π β§ βπ₯ β π (π β π₯) β π β§ βπ₯ β π« π(π₯ βΌ Ο β βͺ π₯
β π)))) β π β (sigAlgebraβπ)) |
49 | 36, 47, 48 | syl56 36 |
. . 3
β’ (π = βͺ
π β (π β βͺ ran
sigAlgebra β π β
(sigAlgebraβπ))) |
50 | 49 | impcom 409 |
. 2
β’ ((π β βͺ ran sigAlgebra β§ π = βͺ π) β π β (sigAlgebraβπ)) |
51 | 13, 50 | impbii 208 |
1
β’ (π β (sigAlgebraβπ) β (π β βͺ ran
sigAlgebra β§ π = βͺ π)) |