Step | Hyp | Ref
| Expression |
1 | | sxsiga 32854 |
. 2
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (π
Γs π)
β βͺ ran sigAlgebra) |
2 | | eqid 2733 |
. . . 4
β’ ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) = ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) |
3 | | eqid 2733 |
. . . 4
β’ βͺ π =
βͺ π |
4 | | eqid 2733 |
. . . 4
β’ βͺ π =
βͺ π |
5 | 2, 3, 4 | txuni2 22939 |
. . 3
β’ (βͺ π
Γ βͺ π) = βͺ ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) |
6 | 2 | sxval 32853 |
. . . . 5
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (π
Γs π) =
(sigaGenβran (π₯
β π, π¦ β π β¦ (π₯ Γ π¦)))) |
7 | 6 | unieqd 4883 |
. . . 4
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β βͺ (π Γs π) = βͺ
(sigaGenβran (π₯
β π, π¦ β π β¦ (π₯ Γ π¦)))) |
8 | | mpoexga 8014 |
. . . . 5
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (π₯
β π, π¦ β π β¦ (π₯ Γ π¦)) β V) |
9 | | rnexg 7845 |
. . . . 5
β’ ((π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β V β ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β V) |
10 | | unisg 32806 |
. . . . 5
β’ (ran
(π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) β V β βͺ (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) = βͺ ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) |
11 | 8, 9, 10 | 3syl 18 |
. . . 4
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β βͺ (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) = βͺ ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) |
12 | 7, 11 | eqtrd 2773 |
. . 3
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β βͺ (π Γs π) = βͺ ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) |
13 | 5, 12 | eqtr4id 2792 |
. 2
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (βͺ π Γ βͺ π) = βͺ
(π Γs
π)) |
14 | | issgon 32786 |
. 2
β’ ((π Γs π) β
(sigAlgebraβ(βͺ π Γ βͺ π)) β ((π Γs π) β βͺ ran
sigAlgebra β§ (βͺ π Γ βͺ π) = βͺ
(π Γs
π))) |
15 | 1, 13, 14 | sylanbrc 584 |
1
β’ ((π β βͺ ran sigAlgebra β§ π β βͺ ran
sigAlgebra) β (π
Γs π)
β (sigAlgebraβ(βͺ π Γ βͺ π))) |