Step | Hyp | Ref
| Expression |
1 | | df-pt 17390 |
. 2
β’
βt = (π β V β¦ (topGenβ{π₯ β£ βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))})) |
2 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β π = πΉ) |
3 | 2 | dmeqd 5906 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β dom π = dom πΉ) |
4 | | fndm 6653 |
. . . . . . . . . . 11
β’ (πΉ Fn π΄ β dom πΉ = π΄) |
5 | 4 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β dom πΉ = π΄) |
6 | 3, 5 | eqtrd 2773 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β dom π = π΄) |
7 | 6 | fneq2d 6644 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (π Fn dom π β π Fn π΄)) |
8 | 2 | fveq1d 6894 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (πβπ¦) = (πΉβπ¦)) |
9 | 8 | eleq2d 2820 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β ((πβπ¦) β (πβπ¦) β (πβπ¦) β (πΉβπ¦))) |
10 | 6, 9 | raleqbidv 3343 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (βπ¦ β dom π(πβπ¦) β (πβπ¦) β βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) |
11 | 6 | difeq1d 4122 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (dom π β π§) = (π΄ β π§)) |
12 | 8 | unieqd 4923 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β βͺ (πβπ¦) = βͺ (πΉβπ¦)) |
13 | 12 | eqeq2d 2744 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β ((πβπ¦) = βͺ (πβπ¦) β (πβπ¦) = βͺ (πΉβπ¦))) |
14 | 11, 13 | raleqbidv 3343 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦) β βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦))) |
15 | 14 | rexbidv 3179 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦) β βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦))) |
16 | 7, 10, 15 | 3anbi123d 1437 |
. . . . . . 7
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)))) |
17 | 6 | ixpeq1d 8903 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β Xπ¦ β dom π(πβπ¦) = Xπ¦ β π΄ (πβπ¦)) |
18 | 17 | eqeq2d 2744 |
. . . . . . 7
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (π₯ = Xπ¦ β dom π(πβπ¦) β π₯ = Xπ¦ β π΄ (πβπ¦))) |
19 | 16, 18 | anbi12d 632 |
. . . . . 6
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦)) β ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)))) |
20 | 19 | exbidv 1925 |
. . . . 5
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦)) β βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)))) |
21 | 20 | abbidv 2802 |
. . . 4
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β {π₯ β£ βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))} = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))}) |
22 | | ptval.1 |
. . . 4
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} |
23 | 21, 22 | eqtr4di 2791 |
. . 3
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β {π₯ β£ βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))} = π΅) |
24 | 23 | fveq2d 6896 |
. 2
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (topGenβ{π₯ β£ βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))}) = (topGenβπ΅)) |
25 | | fnex 7219 |
. . 3
β’ ((πΉ Fn π΄ β§ π΄ β π) β πΉ β V) |
26 | 25 | ancoms 460 |
. 2
β’ ((π΄ β π β§ πΉ Fn π΄) β πΉ β V) |
27 | | fvexd 6907 |
. 2
β’ ((π΄ β π β§ πΉ Fn π΄) β (topGenβπ΅) β V) |
28 | 1, 24, 26, 27 | fvmptd2 7007 |
1
β’ ((π΄ β π β§ πΉ Fn π΄) β (βtβπΉ) = (topGenβπ΅)) |