Step | Hyp | Ref
| Expression |
1 | | df-pt 17386 |
. 2
β’
βt = (π β V β¦ (topGenβ{π₯ β£ βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))})) |
2 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β π = πΉ) |
3 | 2 | dmeqd 5903 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β dom π = dom πΉ) |
4 | | fndm 6649 |
. . . . . . . . . . 11
β’ (πΉ Fn π΄ β dom πΉ = π΄) |
5 | 4 | ad2antlr 725 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β dom πΉ = π΄) |
6 | 3, 5 | eqtrd 2772 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β dom π = π΄) |
7 | 6 | fneq2d 6640 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (π Fn dom π β π Fn π΄)) |
8 | 2 | fveq1d 6890 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (πβπ¦) = (πΉβπ¦)) |
9 | 8 | eleq2d 2819 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β ((πβπ¦) β (πβπ¦) β (πβπ¦) β (πΉβπ¦))) |
10 | 6, 9 | raleqbidv 3342 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (βπ¦ β dom π(πβπ¦) β (πβπ¦) β βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) |
11 | 6 | difeq1d 4120 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (dom π β π§) = (π΄ β π§)) |
12 | 8 | unieqd 4921 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β βͺ (πβπ¦) = βͺ (πΉβπ¦)) |
13 | 12 | eqeq2d 2743 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β ((πβπ¦) = βͺ (πβπ¦) β (πβπ¦) = βͺ (πΉβπ¦))) |
14 | 11, 13 | raleqbidv 3342 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦) β βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦))) |
15 | 14 | rexbidv 3178 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦) β βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦))) |
16 | 7, 10, 15 | 3anbi123d 1436 |
. . . . . . 7
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)))) |
17 | 6 | ixpeq1d 8899 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β Xπ¦ β dom π(πβπ¦) = Xπ¦ β π΄ (πβπ¦)) |
18 | 17 | eqeq2d 2743 |
. . . . . . 7
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (π₯ = Xπ¦ β dom π(πβπ¦) β π₯ = Xπ¦ β π΄ (πβπ¦))) |
19 | 16, 18 | anbi12d 631 |
. . . . . 6
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦)) β ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)))) |
20 | 19 | exbidv 1924 |
. . . . 5
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦)) β βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦)))) |
21 | 20 | abbidv 2801 |
. . . 4
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β {π₯ β£ βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))} = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))}) |
22 | | ptval.1 |
. . . 4
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} |
23 | 21, 22 | eqtr4di 2790 |
. . 3
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β {π₯ β£ βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))} = π΅) |
24 | 23 | fveq2d 6892 |
. 2
β’ (((π΄ β π β§ πΉ Fn π΄) β§ π = πΉ) β (topGenβ{π₯ β£ βπ((π Fn dom π β§ βπ¦ β dom π(πβπ¦) β (πβπ¦) β§ βπ§ β Fin βπ¦ β (dom π β π§)(πβπ¦) = βͺ (πβπ¦)) β§ π₯ = Xπ¦ β dom π(πβπ¦))}) = (topGenβπ΅)) |
25 | | fnex 7215 |
. . 3
β’ ((πΉ Fn π΄ β§ π΄ β π) β πΉ β V) |
26 | 25 | ancoms 459 |
. 2
β’ ((π΄ β π β§ πΉ Fn π΄) β πΉ β V) |
27 | | fvexd 6903 |
. 2
β’ ((π΄ β π β§ πΉ Fn π΄) β (topGenβπ΅) β V) |
28 | 1, 24, 26, 27 | fvmptd2 7003 |
1
β’ ((π΄ β π β§ πΉ Fn π΄) β (βtβπΉ) = (topGenβπ΅)) |