Step | Hyp | Ref
| Expression |
1 | | pwsiga 33128 |
. . . . . 6
β’ (π β π β π« π β (sigAlgebraβπ)) |
2 | | elrnsiga 33124 |
. . . . . 6
β’
(π« π β
(sigAlgebraβπ) β
π« π β βͺ ran sigAlgebra) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β π β π« π β βͺ ran
sigAlgebra) |
4 | | brsigarn 33182 |
. . . . . 6
β’
π
β β
(sigAlgebraββ) |
5 | | elrnsiga 33124 |
. . . . . 6
β’
(π
β β (sigAlgebraββ) β
π
β β βͺ ran
sigAlgebra) |
6 | 4, 5 | mp1i 13 |
. . . . 5
β’ (π β π β π
β β
βͺ ran sigAlgebra) |
7 | 3, 6 | ismbfm 33249 |
. . . 4
β’ (π β π β (π β (π« πMblFnMπ
β) β
(π β (βͺ π
β βm βͺ π« π) β§ βπ₯ β π
β (β‘π β π₯) β π« π))) |
8 | | unibrsiga 33184 |
. . . . . . . . . 10
β’ βͺ π
β = β |
9 | | reex 11201 |
. . . . . . . . . 10
β’ β
β V |
10 | 8, 9 | eqeltri 2830 |
. . . . . . . . 9
β’ βͺ π
β β V |
11 | | unipw 5451 |
. . . . . . . . . 10
β’ βͺ π« π = π |
12 | | elex 3493 |
. . . . . . . . . 10
β’ (π β π β π β V) |
13 | 11, 12 | eqeltrid 2838 |
. . . . . . . . 9
β’ (π β π β βͺ
π« π β
V) |
14 | | elmapg 8833 |
. . . . . . . . 9
β’ ((βͺ π
β β V β§ βͺ π« π β V) β (π β (βͺ
π
β βm βͺ
π« π) β π:βͺ
π« πβΆβͺ π
β)) |
15 | 10, 13, 14 | sylancr 588 |
. . . . . . . 8
β’ (π β π β (π β (βͺ
π
β βm βͺ
π« π) β π:βͺ
π« πβΆβͺ π
β)) |
16 | 11 | feq2i 6710 |
. . . . . . . 8
β’ (π:βͺ
π« πβΆβͺ π
β β π:πβΆβͺ
π
β) |
17 | 15, 16 | bitrdi 287 |
. . . . . . 7
β’ (π β π β (π β (βͺ
π
β βm βͺ
π« π) β π:πβΆβͺ
π
β)) |
18 | | ffn 6718 |
. . . . . . 7
β’ (π:πβΆβͺ
π
β β π Fn π) |
19 | 17, 18 | syl6bi 253 |
. . . . . 6
β’ (π β π β (π β (βͺ
π
β βm βͺ
π« π) β π Fn π)) |
20 | | elpreima 7060 |
. . . . . . . . . 10
β’ (π Fn π β (π¦ β (β‘π β π₯) β (π¦ β π β§ (πβπ¦) β π₯))) |
21 | | simpl 484 |
. . . . . . . . . 10
β’ ((π¦ β π β§ (πβπ¦) β π₯) β π¦ β π) |
22 | 20, 21 | syl6bi 253 |
. . . . . . . . 9
β’ (π Fn π β (π¦ β (β‘π β π₯) β π¦ β π)) |
23 | 22 | ssrdv 3989 |
. . . . . . . 8
β’ (π Fn π β (β‘π β π₯) β π) |
24 | | vex 3479 |
. . . . . . . . . . 11
β’ π β V |
25 | 24 | cnvex 7916 |
. . . . . . . . . 10
β’ β‘π β V |
26 | | imaexg 7906 |
. . . . . . . . . 10
β’ (β‘π β V β (β‘π β π₯) β V) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . 9
β’ (β‘π β π₯) β V |
28 | 27 | elpw 4607 |
. . . . . . . 8
β’ ((β‘π β π₯) β π« π β (β‘π β π₯) β π) |
29 | 23, 28 | sylibr 233 |
. . . . . . 7
β’ (π Fn π β (β‘π β π₯) β π« π) |
30 | 29 | ralrimivw 3151 |
. . . . . 6
β’ (π Fn π β βπ₯ β π
β (β‘π β π₯) β π« π) |
31 | 19, 30 | syl6 35 |
. . . . 5
β’ (π β π β (π β (βͺ
π
β βm βͺ
π« π) β
βπ₯ β
π
β (β‘π β π₯) β π« π)) |
32 | 31 | pm4.71d 563 |
. . . 4
β’ (π β π β (π β (βͺ
π
β βm βͺ
π« π) β (π β (βͺ π
β βm βͺ π« π) β§ βπ₯ β π
β (β‘π β π₯) β π« π))) |
33 | 7, 32 | bitr4d 282 |
. . 3
β’ (π β π β (π β (π« πMblFnMπ
β) β
π β (βͺ π
β βm βͺ π« π))) |
34 | 33 | eqrdv 2731 |
. 2
β’ (π β π β (π« πMblFnMπ
β) = (βͺ π
β βm βͺ π« π)) |
35 | 8, 11 | oveq12i 7421 |
. 2
β’ (βͺ π
β βm βͺ π« π) = (β βm π) |
36 | 34, 35 | eqtrdi 2789 |
1
β’ (π β π β (π« πMblFnMπ
β) =
(β βm π)) |