Step | Hyp | Ref
| Expression |
1 | | mofeu.2 |
. . . . 5
β’ (π β (π΅ = β
β π΄ = β
)) |
2 | 1 | imp 408 |
. . . 4
β’ ((π β§ π΅ = β
) β π΄ = β
) |
3 | | f00 6774 |
. . . . 5
β’ (πΉ:π΄βΆβ
β (πΉ = β
β§ π΄ = β
)) |
4 | 3 | rbaib 540 |
. . . 4
β’ (π΄ = β
β (πΉ:π΄βΆβ
β πΉ = β
)) |
5 | 2, 4 | syl 17 |
. . 3
β’ ((π β§ π΅ = β
) β (πΉ:π΄βΆβ
β πΉ = β
)) |
6 | | feq3 6701 |
. . . 4
β’ (π΅ = β
β (πΉ:π΄βΆπ΅ β πΉ:π΄βΆβ
)) |
7 | 6 | adantl 483 |
. . 3
β’ ((π β§ π΅ = β
) β (πΉ:π΄βΆπ΅ β πΉ:π΄βΆβ
)) |
8 | | mofeu.1 |
. . . . . 6
β’ πΊ = (π΄ Γ π΅) |
9 | | xpeq2 5698 |
. . . . . . 7
β’ (π΅ = β
β (π΄ Γ π΅) = (π΄ Γ β
)) |
10 | | xp0 6158 |
. . . . . . 7
β’ (π΄ Γ β
) =
β
|
11 | 9, 10 | eqtrdi 2789 |
. . . . . 6
β’ (π΅ = β
β (π΄ Γ π΅) = β
) |
12 | 8, 11 | eqtrid 2785 |
. . . . 5
β’ (π΅ = β
β πΊ = β
) |
13 | 12 | adantl 483 |
. . . 4
β’ ((π β§ π΅ = β
) β πΊ = β
) |
14 | 13 | eqeq2d 2744 |
. . 3
β’ ((π β§ π΅ = β
) β (πΉ = πΊ β πΉ = β
)) |
15 | 5, 7, 14 | 3bitr4d 311 |
. 2
β’ ((π β§ π΅ = β
) β (πΉ:π΄βΆπ΅ β πΉ = πΊ)) |
16 | | 19.42v 1958 |
. . 3
β’
(βπ¦(π β§ π΅ = {π¦}) β (π β§ βπ¦ π΅ = {π¦})) |
17 | | fconst2g 7204 |
. . . . . . . 8
β’ (π¦ β V β (πΉ:π΄βΆ{π¦} β πΉ = (π΄ Γ {π¦}))) |
18 | 17 | elv 3481 |
. . . . . . 7
β’ (πΉ:π΄βΆ{π¦} β πΉ = (π΄ Γ {π¦})) |
19 | | feq3 6701 |
. . . . . . . 8
β’ (π΅ = {π¦} β (πΉ:π΄βΆπ΅ β πΉ:π΄βΆ{π¦})) |
20 | | xpeq2 5698 |
. . . . . . . . 9
β’ (π΅ = {π¦} β (π΄ Γ π΅) = (π΄ Γ {π¦})) |
21 | 20 | eqeq2d 2744 |
. . . . . . . 8
β’ (π΅ = {π¦} β (πΉ = (π΄ Γ π΅) β πΉ = (π΄ Γ {π¦}))) |
22 | 19, 21 | bibi12d 346 |
. . . . . . 7
β’ (π΅ = {π¦} β ((πΉ:π΄βΆπ΅ β πΉ = (π΄ Γ π΅)) β (πΉ:π΄βΆ{π¦} β πΉ = (π΄ Γ {π¦})))) |
23 | 18, 22 | mpbiri 258 |
. . . . . 6
β’ (π΅ = {π¦} β (πΉ:π΄βΆπ΅ β πΉ = (π΄ Γ π΅))) |
24 | 8 | eqeq2i 2746 |
. . . . . 6
β’ (πΉ = πΊ β πΉ = (π΄ Γ π΅)) |
25 | 23, 24 | bitr4di 289 |
. . . . 5
β’ (π΅ = {π¦} β (πΉ:π΄βΆπ΅ β πΉ = πΊ)) |
26 | 25 | adantl 483 |
. . . 4
β’ ((π β§ π΅ = {π¦}) β (πΉ:π΄βΆπ΅ β πΉ = πΊ)) |
27 | 26 | exlimiv 1934 |
. . 3
β’
(βπ¦(π β§ π΅ = {π¦}) β (πΉ:π΄βΆπ΅ β πΉ = πΊ)) |
28 | 16, 27 | sylbir 234 |
. 2
β’ ((π β§ βπ¦ π΅ = {π¦}) β (πΉ:π΄βΆπ΅ β πΉ = πΊ)) |
29 | | mofeu.3 |
. . 3
β’ (π β β*π₯ π₯ β π΅) |
30 | | mo0sn 47500 |
. . 3
β’
(β*π₯ π₯ β π΅ β (π΅ = β
β¨ βπ¦ π΅ = {π¦})) |
31 | 29, 30 | sylib 217 |
. 2
β’ (π β (π΅ = β
β¨ βπ¦ π΅ = {π¦})) |
32 | 15, 28, 31 | mpjaodan 958 |
1
β’ (π β (πΉ:π΄βΆπ΅ β πΉ = πΊ)) |