Step | Hyp | Ref
| Expression |
1 | | elex 3461 |
. . 3
β’ (π β π β π β V) |
2 | | elex 3461 |
. . 3
β’ (π β π β π β V) |
3 | | id 22 |
. . . . . . 7
β’ (π = π β π = π) |
4 | | eqidd 2738 |
. . . . . . 7
β’ (π = π β π‘ = π‘) |
5 | | eqidd 2738 |
. . . . . . 7
β’ (π = π β (π₯ Γ π¦) = (π₯ Γ π¦)) |
6 | 3, 4, 5 | mpoeq123dv 7426 |
. . . . . 6
β’ (π = π β (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦)) = (π₯ β π, π¦ β π‘ β¦ (π₯ Γ π¦))) |
7 | 6 | rneqd 5891 |
. . . . 5
β’ (π = π β ran (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦)) = ran (π₯ β π, π¦ β π‘ β¦ (π₯ Γ π¦))) |
8 | 7 | fveq2d 6843 |
. . . 4
β’ (π = π β (sigaGenβran (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦))) = (sigaGenβran (π₯ β π, π¦ β π‘ β¦ (π₯ Γ π¦)))) |
9 | | eqidd 2738 |
. . . . . . 7
β’ (π‘ = π β π = π) |
10 | | id 22 |
. . . . . . 7
β’ (π‘ = π β π‘ = π) |
11 | | eqidd 2738 |
. . . . . . 7
β’ (π‘ = π β (π₯ Γ π¦) = (π₯ Γ π¦)) |
12 | 9, 10, 11 | mpoeq123dv 7426 |
. . . . . 6
β’ (π‘ = π β (π₯ β π, π¦ β π‘ β¦ (π₯ Γ π¦)) = (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) |
13 | 12 | rneqd 5891 |
. . . . 5
β’ (π‘ = π β ran (π₯ β π, π¦ β π‘ β¦ (π₯ Γ π¦)) = ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) |
14 | 13 | fveq2d 6843 |
. . . 4
β’ (π‘ = π β (sigaGenβran (π₯ β π, π¦ β π‘ β¦ (π₯ Γ π¦))) = (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
15 | | df-sx 32600 |
. . . 4
β’
Γs = (π
β V, π‘ β V
β¦ (sigaGenβran (π₯ β π , π¦ β π‘ β¦ (π₯ Γ π¦)))) |
16 | | fvex 6852 |
. . . 4
β’
(sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦))) β V |
17 | 8, 14, 15, 16 | ovmpo 7509 |
. . 3
β’ ((π β V β§ π β V) β (π Γs π) = (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
18 | 1, 2, 17 | syl2an 596 |
. 2
β’ ((π β π β§ π β π) β (π Γs π) = (sigaGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) |
19 | | sxval.1 |
. . 3
β’ π΄ = ran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)) |
20 | 19 | fveq2i 6842 |
. 2
β’
(sigaGenβπ΄) =
(sigaGenβran (π₯
β π, π¦ β π β¦ (π₯ Γ π¦))) |
21 | 18, 20 | eqtr4di 2795 |
1
β’ ((π β π β§ π β π) β (π Γs π) = (sigaGenβπ΄)) |