Step | Hyp | Ref
| Expression |
1 | | dvmptres3.s |
. . 3
β’ (π β π β {β, β}) |
2 | | dvmptres3.a |
. . . 4
β’ ((π β§ π₯ β π) β π΄ β β) |
3 | 2 | fmpttd 7067 |
. . 3
β’ (π β (π₯ β π β¦ π΄):πβΆβ) |
4 | | dvmptres3.x |
. . 3
β’ (π β π β π½) |
5 | | dvmptres3.d |
. . . . 5
β’ (π β (β D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |
6 | 5 | dmeqd 5865 |
. . . 4
β’ (π β dom (β D (π₯ β π β¦ π΄)) = dom (π₯ β π β¦ π΅)) |
7 | | eqid 2733 |
. . . . 5
β’ (π₯ β π β¦ π΅) = (π₯ β π β¦ π΅) |
8 | | dvmptres3.b |
. . . . 5
β’ ((π β§ π₯ β π) β π΅ β π) |
9 | 7, 8 | dmmptd 6650 |
. . . 4
β’ (π β dom (π₯ β π β¦ π΅) = π) |
10 | 6, 9 | eqtrd 2773 |
. . 3
β’ (π β dom (β D (π₯ β π β¦ π΄)) = π) |
11 | | dvmptres3.j |
. . . 4
β’ π½ =
(TopOpenββfld) |
12 | 11 | dvres3a 25301 |
. . 3
β’ (((π β {β, β} β§
(π₯ β π β¦ π΄):πβΆβ) β§ (π β π½ β§ dom (β D (π₯ β π β¦ π΄)) = π)) β (π D ((π₯ β π β¦ π΄) βΎ π)) = ((β D (π₯ β π β¦ π΄)) βΎ π)) |
13 | 1, 3, 4, 10, 12 | syl22anc 838 |
. 2
β’ (π β (π D ((π₯ β π β¦ π΄) βΎ π)) = ((β D (π₯ β π β¦ π΄)) βΎ π)) |
14 | | rescom 5967 |
. . . . . 6
β’ (((π₯ β π β¦ π΄) βΎ π) βΎ π) = (((π₯ β π β¦ π΄) βΎ π) βΎ π) |
15 | | resres 5954 |
. . . . . 6
β’ (((π₯ β π β¦ π΄) βΎ π) βΎ π) = ((π₯ β π β¦ π΄) βΎ (π β© π)) |
16 | 14, 15 | eqtri 2761 |
. . . . 5
β’ (((π₯ β π β¦ π΄) βΎ π) βΎ π) = ((π₯ β π β¦ π΄) βΎ (π β© π)) |
17 | | dvmptres3.y |
. . . . . 6
β’ (π β (π β© π) = π) |
18 | 17 | reseq2d 5941 |
. . . . 5
β’ (π β ((π₯ β π β¦ π΄) βΎ (π β© π)) = ((π₯ β π β¦ π΄) βΎ π)) |
19 | 16, 18 | eqtrid 2785 |
. . . 4
β’ (π β (((π₯ β π β¦ π΄) βΎ π) βΎ π) = ((π₯ β π β¦ π΄) βΎ π)) |
20 | | ffn 6672 |
. . . . . 6
β’ ((π₯ β π β¦ π΄):πβΆβ β (π₯ β π β¦ π΄) Fn π) |
21 | | fnresdm 6624 |
. . . . . 6
β’ ((π₯ β π β¦ π΄) Fn π β ((π₯ β π β¦ π΄) βΎ π) = (π₯ β π β¦ π΄)) |
22 | 3, 20, 21 | 3syl 18 |
. . . . 5
β’ (π β ((π₯ β π β¦ π΄) βΎ π) = (π₯ β π β¦ π΄)) |
23 | 22 | reseq1d 5940 |
. . . 4
β’ (π β (((π₯ β π β¦ π΄) βΎ π) βΎ π) = ((π₯ β π β¦ π΄) βΎ π)) |
24 | | inss2 4193 |
. . . . . 6
β’ (π β© π) β π |
25 | 17, 24 | eqsstrrdi 4003 |
. . . . 5
β’ (π β π β π) |
26 | 25 | resmptd 5998 |
. . . 4
β’ (π β ((π₯ β π β¦ π΄) βΎ π) = (π₯ β π β¦ π΄)) |
27 | 19, 23, 26 | 3eqtr3d 2781 |
. . 3
β’ (π β ((π₯ β π β¦ π΄) βΎ π) = (π₯ β π β¦ π΄)) |
28 | 27 | oveq2d 7377 |
. 2
β’ (π β (π D ((π₯ β π β¦ π΄) βΎ π)) = (π D (π₯ β π β¦ π΄))) |
29 | | rescom 5967 |
. . . . 5
β’ (((π₯ β π β¦ π΅) βΎ π) βΎ π) = (((π₯ β π β¦ π΅) βΎ π) βΎ π) |
30 | | resres 5954 |
. . . . 5
β’ (((π₯ β π β¦ π΅) βΎ π) βΎ π) = ((π₯ β π β¦ π΅) βΎ (π β© π)) |
31 | 29, 30 | eqtri 2761 |
. . . 4
β’ (((π₯ β π β¦ π΅) βΎ π) βΎ π) = ((π₯ β π β¦ π΅) βΎ (π β© π)) |
32 | 17 | reseq2d 5941 |
. . . 4
β’ (π β ((π₯ β π β¦ π΅) βΎ (π β© π)) = ((π₯ β π β¦ π΅) βΎ π)) |
33 | 31, 32 | eqtrid 2785 |
. . 3
β’ (π β (((π₯ β π β¦ π΅) βΎ π) βΎ π) = ((π₯ β π β¦ π΅) βΎ π)) |
34 | 8 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ₯ β π π΅ β π) |
35 | 7 | fnmpt 6645 |
. . . . . 6
β’
(βπ₯ β
π π΅ β π β (π₯ β π β¦ π΅) Fn π) |
36 | | fnresdm 6624 |
. . . . . 6
β’ ((π₯ β π β¦ π΅) Fn π β ((π₯ β π β¦ π΅) βΎ π) = (π₯ β π β¦ π΅)) |
37 | 34, 35, 36 | 3syl 18 |
. . . . 5
β’ (π β ((π₯ β π β¦ π΅) βΎ π) = (π₯ β π β¦ π΅)) |
38 | 37, 5 | eqtr4d 2776 |
. . . 4
β’ (π β ((π₯ β π β¦ π΅) βΎ π) = (β D (π₯ β π β¦ π΄))) |
39 | 38 | reseq1d 5940 |
. . 3
β’ (π β (((π₯ β π β¦ π΅) βΎ π) βΎ π) = ((β D (π₯ β π β¦ π΄)) βΎ π)) |
40 | 25 | resmptd 5998 |
. . 3
β’ (π β ((π₯ β π β¦ π΅) βΎ π) = (π₯ β π β¦ π΅)) |
41 | 33, 39, 40 | 3eqtr3d 2781 |
. 2
β’ (π β ((β D (π₯ β π β¦ π΄)) βΎ π) = (π₯ β π β¦ π΅)) |
42 | 13, 28, 41 | 3eqtr3d 2781 |
1
β’ (π β (π D (π₯ β π β¦ π΄)) = (π₯ β π β¦ π΅)) |