Step | Hyp | Ref
| Expression |
1 | | mbfmco.1 |
. . . . . . 7
β’ (π β π
β βͺ ran
sigAlgebra) |
2 | | mbfmco.2 |
. . . . . . 7
β’ (π β π β βͺ ran
sigAlgebra) |
3 | | mbfmco2.4 |
. . . . . . 7
β’ (π β πΉ β (π
MblFnMπ)) |
4 | 1, 2, 3 | mbfmf 33247 |
. . . . . 6
β’ (π β πΉ:βͺ π
βΆβͺ π) |
5 | 4 | ffvelcdmda 7086 |
. . . . 5
β’ ((π β§ π₯ β βͺ π
) β (πΉβπ₯) β βͺ π) |
6 | | mbfmco.3 |
. . . . . . 7
β’ (π β π β βͺ ran
sigAlgebra) |
7 | | mbfmco2.5 |
. . . . . . 7
β’ (π β πΊ β (π
MblFnMπ)) |
8 | 1, 6, 7 | mbfmf 33247 |
. . . . . 6
β’ (π β πΊ:βͺ π
βΆβͺ π) |
9 | 8 | ffvelcdmda 7086 |
. . . . 5
β’ ((π β§ π₯ β βͺ π
) β (πΊβπ₯) β βͺ π) |
10 | | opelxpi 5713 |
. . . . 5
β’ (((πΉβπ₯) β βͺ π β§ (πΊβπ₯) β βͺ π) β β¨(πΉβπ₯), (πΊβπ₯)β© β (βͺ
π Γ βͺ π)) |
11 | 5, 9, 10 | syl2anc 584 |
. . . 4
β’ ((π β§ π₯ β βͺ π
) β β¨(πΉβπ₯), (πΊβπ₯)β© β (βͺ
π Γ βͺ π)) |
12 | | sxuni 33186 |
. . . . . 6
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (βͺ π Γ βͺ π) = βͺ
(π Γs
π)) |
13 | 2, 6, 12 | syl2anc 584 |
. . . . 5
β’ (π β (βͺ π
Γ βͺ π) = βͺ (π Γs π)) |
14 | 13 | adantr 481 |
. . . 4
β’ ((π β§ π₯ β βͺ π
) β (βͺ π
Γ βͺ π) = βͺ (π Γs π)) |
15 | 11, 14 | eleqtrd 2835 |
. . 3
β’ ((π β§ π₯ β βͺ π
) β β¨(πΉβπ₯), (πΊβπ₯)β© β βͺ
(π Γs
π)) |
16 | | mbfmco2.6 |
. . 3
β’ π» = (π₯ β βͺ π
β¦ β¨(πΉβπ₯), (πΊβπ₯)β©) |
17 | 15, 16 | fmptd 7113 |
. 2
β’ (π β π»:βͺ π
βΆβͺ (π
Γs π)) |
18 | | eqid 2732 |
. . . . 5
β’ (π β π, π β π β¦ (π Γ π)) = (π β π, π β π β¦ (π Γ π)) |
19 | | vex 3478 |
. . . . . 6
β’ π β V |
20 | | vex 3478 |
. . . . . 6
β’ π β V |
21 | 19, 20 | xpex 7739 |
. . . . 5
β’ (π Γ π) β V |
22 | 18, 21 | elrnmpo 7544 |
. . . 4
β’ (π β ran (π β π, π β π β¦ (π Γ π)) β βπ β π βπ β π π = (π Γ π)) |
23 | | simp3 1138 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π) β§ π = (π Γ π)) β π = (π Γ π)) |
24 | 23 | imaeq2d 6059 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π) β§ π = (π Γ π)) β (β‘π» β π) = (β‘π» β (π Γ π))) |
25 | | simp1 1136 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π) β§ π = (π Γ π)) β π) |
26 | | simp2l 1199 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π) β§ π = (π Γ π)) β π β π) |
27 | | simp2r 1200 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β π) β§ π = (π Γ π)) β π β π) |
28 | 4, 8, 16 | xppreima2 31871 |
. . . . . . . . . . 11
β’ (π β (β‘π» β (π Γ π)) = ((β‘πΉ β π) β© (β‘πΊ β π))) |
29 | 28 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ π β π) β (β‘π» β (π Γ π)) = ((β‘πΉ β π) β© (β‘πΊ β π))) |
30 | 1 | 3ad2ant1 1133 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ π β π) β π
β βͺ ran
sigAlgebra) |
31 | 2 | 3ad2ant1 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β π) β π β βͺ ran
sigAlgebra) |
32 | 3 | 3ad2ant1 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β π) β πΉ β (π
MblFnMπ)) |
33 | | simp2 1137 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β π) β π β π) |
34 | 30, 31, 32, 33 | mbfmcnvima 33249 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ π β π) β (β‘πΉ β π) β π
) |
35 | 6 | 3ad2ant1 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β π) β π β βͺ ran
sigAlgebra) |
36 | 7 | 3ad2ant1 1133 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β π) β πΊ β (π
MblFnMπ)) |
37 | | simp3 1138 |
. . . . . . . . . . . 12
β’ ((π β§ π β π β§ π β π) β π β π) |
38 | 30, 35, 36, 37 | mbfmcnvima 33249 |
. . . . . . . . . . 11
β’ ((π β§ π β π β§ π β π) β (β‘πΊ β π) β π
) |
39 | | inelsiga 33128 |
. . . . . . . . . . 11
β’ ((π
β βͺ ran sigAlgebra β§ (β‘πΉ β π) β π
β§ (β‘πΊ β π) β π
) β ((β‘πΉ β π) β© (β‘πΊ β π)) β π
) |
40 | 30, 34, 38, 39 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((π β§ π β π β§ π β π) β ((β‘πΉ β π) β© (β‘πΊ β π)) β π
) |
41 | 29, 40 | eqeltrd 2833 |
. . . . . . . . 9
β’ ((π β§ π β π β§ π β π) β (β‘π» β (π Γ π)) β π
) |
42 | 25, 26, 27, 41 | syl3anc 1371 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β π) β§ π = (π Γ π)) β (β‘π» β (π Γ π)) β π
) |
43 | 24, 42 | eqeltrd 2833 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β π) β§ π = (π Γ π)) β (β‘π» β π) β π
) |
44 | 43 | 3expia 1121 |
. . . . . 6
β’ ((π β§ (π β π β§ π β π)) β (π = (π Γ π) β (β‘π» β π) β π
)) |
45 | 44 | rexlimdvva 3211 |
. . . . 5
β’ (π β (βπ β π βπ β π π = (π Γ π) β (β‘π» β π) β π
)) |
46 | 45 | imp 407 |
. . . 4
β’ ((π β§ βπ β π βπ β π π = (π Γ π)) β (β‘π» β π) β π
) |
47 | 22, 46 | sylan2b 594 |
. . 3
β’ ((π β§ π β ran (π β π, π β π β¦ (π Γ π))) β (β‘π» β π) β π
) |
48 | 47 | ralrimiva 3146 |
. 2
β’ (π β βπ β ran (π β π, π β π β¦ (π Γ π))(β‘π» β π) β π
) |
49 | | eqid 2732 |
. . . . 5
β’ ran
(π β π, π β π β¦ (π Γ π)) = ran (π β π, π β π β¦ (π Γ π)) |
50 | 49 | txbasex 23069 |
. . . 4
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β ran (π
β π, π β π β¦ (π Γ π)) β V) |
51 | 2, 6, 50 | syl2anc 584 |
. . 3
β’ (π β ran (π β π, π β π β¦ (π Γ π)) β V) |
52 | 49 | sxval 33183 |
. . . 4
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (π
Γs π) =
(sigaGenβran (π
β π, π β π β¦ (π Γ π)))) |
53 | 2, 6, 52 | syl2anc 584 |
. . 3
β’ (π β (π Γs π) = (sigaGenβran (π β π, π β π β¦ (π Γ π)))) |
54 | 51, 1, 53 | imambfm 33256 |
. 2
β’ (π β (π» β (π
MblFnM(π Γs π)) β (π»:βͺ π
βΆβͺ (π
Γs π)
β§ βπ β ran
(π β π, π β π β¦ (π Γ π))(β‘π» β π) β π
))) |
55 | 17, 48, 54 | mpbir2and 711 |
1
β’ (π β π» β (π
MblFnM(π Γs π))) |