Step |
Hyp |
Ref |
Expression |
1 |
|
dvmptco.s |
โข ( ๐ โ ๐ โ { โ , โ } ) |
2 |
|
dvmptco.t |
โข ( ๐ โ ๐ โ { โ , โ } ) |
3 |
|
dvmptco.a |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ๐ด โ ๐ ) |
4 |
|
dvmptco.b |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ๐ต โ ๐ ) |
5 |
|
dvmptco.c |
โข ( ( ๐ โง ๐ฆ โ ๐ ) โ ๐ถ โ โ ) |
6 |
|
dvmptco.d |
โข ( ( ๐ โง ๐ฆ โ ๐ ) โ ๐ท โ ๐ ) |
7 |
|
dvmptco.da |
โข ( ๐ โ ( ๐ D ( ๐ฅ โ ๐ โฆ ๐ด ) ) = ( ๐ฅ โ ๐ โฆ ๐ต ) ) |
8 |
|
dvmptco.dc |
โข ( ๐ โ ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) = ( ๐ฆ โ ๐ โฆ ๐ท ) ) |
9 |
|
dvmptco.e |
โข ( ๐ฆ = ๐ด โ ๐ถ = ๐ธ ) |
10 |
|
dvmptco.f |
โข ( ๐ฆ = ๐ด โ ๐ท = ๐น ) |
11 |
5
|
fmpttd |
โข ( ๐ โ ( ๐ฆ โ ๐ โฆ ๐ถ ) : ๐ โถ โ ) |
12 |
3
|
fmpttd |
โข ( ๐ โ ( ๐ฅ โ ๐ โฆ ๐ด ) : ๐ โถ ๐ ) |
13 |
8
|
dmeqd |
โข ( ๐ โ dom ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) = dom ( ๐ฆ โ ๐ โฆ ๐ท ) ) |
14 |
6
|
ralrimiva |
โข ( ๐ โ โ ๐ฆ โ ๐ ๐ท โ ๐ ) |
15 |
|
dmmptg |
โข ( โ ๐ฆ โ ๐ ๐ท โ ๐ โ dom ( ๐ฆ โ ๐ โฆ ๐ท ) = ๐ ) |
16 |
14 15
|
syl |
โข ( ๐ โ dom ( ๐ฆ โ ๐ โฆ ๐ท ) = ๐ ) |
17 |
13 16
|
eqtrd |
โข ( ๐ โ dom ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) = ๐ ) |
18 |
7
|
dmeqd |
โข ( ๐ โ dom ( ๐ D ( ๐ฅ โ ๐ โฆ ๐ด ) ) = dom ( ๐ฅ โ ๐ โฆ ๐ต ) ) |
19 |
4
|
ralrimiva |
โข ( ๐ โ โ ๐ฅ โ ๐ ๐ต โ ๐ ) |
20 |
|
dmmptg |
โข ( โ ๐ฅ โ ๐ ๐ต โ ๐ โ dom ( ๐ฅ โ ๐ โฆ ๐ต ) = ๐ ) |
21 |
19 20
|
syl |
โข ( ๐ โ dom ( ๐ฅ โ ๐ โฆ ๐ต ) = ๐ ) |
22 |
18 21
|
eqtrd |
โข ( ๐ โ dom ( ๐ D ( ๐ฅ โ ๐ โฆ ๐ด ) ) = ๐ ) |
23 |
2 1 11 12 17 22
|
dvcof |
โข ( ๐ โ ( ๐ D ( ( ๐ฆ โ ๐ โฆ ๐ถ ) โ ( ๐ฅ โ ๐ โฆ ๐ด ) ) ) = ( ( ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) โ ( ๐ฅ โ ๐ โฆ ๐ด ) ) โf ยท ( ๐ D ( ๐ฅ โ ๐ โฆ ๐ด ) ) ) ) |
24 |
|
eqidd |
โข ( ๐ โ ( ๐ฅ โ ๐ โฆ ๐ด ) = ( ๐ฅ โ ๐ โฆ ๐ด ) ) |
25 |
|
eqidd |
โข ( ๐ โ ( ๐ฆ โ ๐ โฆ ๐ถ ) = ( ๐ฆ โ ๐ โฆ ๐ถ ) ) |
26 |
3 24 25 9
|
fmptco |
โข ( ๐ โ ( ( ๐ฆ โ ๐ โฆ ๐ถ ) โ ( ๐ฅ โ ๐ โฆ ๐ด ) ) = ( ๐ฅ โ ๐ โฆ ๐ธ ) ) |
27 |
26
|
oveq2d |
โข ( ๐ โ ( ๐ D ( ( ๐ฆ โ ๐ โฆ ๐ถ ) โ ( ๐ฅ โ ๐ โฆ ๐ด ) ) ) = ( ๐ D ( ๐ฅ โ ๐ โฆ ๐ธ ) ) ) |
28 |
|
ovex |
โข ( ๐ D ( ๐ฅ โ ๐ โฆ ๐ด ) ) โ V |
29 |
28
|
dmex |
โข dom ( ๐ D ( ๐ฅ โ ๐ โฆ ๐ด ) ) โ V |
30 |
22 29
|
eqeltrrdi |
โข ( ๐ โ ๐ โ V ) |
31 |
2 5 6 8
|
dvmptcl |
โข ( ( ๐ โง ๐ฆ โ ๐ ) โ ๐ท โ โ ) |
32 |
8 31
|
fmpt3d |
โข ( ๐ โ ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) : ๐ โถ โ ) |
33 |
|
fco |
โข ( ( ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) : ๐ โถ โ โง ( ๐ฅ โ ๐ โฆ ๐ด ) : ๐ โถ ๐ ) โ ( ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) โ ( ๐ฅ โ ๐ โฆ ๐ด ) ) : ๐ โถ โ ) |
34 |
32 12 33
|
syl2anc |
โข ( ๐ โ ( ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) โ ( ๐ฅ โ ๐ โฆ ๐ด ) ) : ๐ โถ โ ) |
35 |
3 24 8 10
|
fmptco |
โข ( ๐ โ ( ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) โ ( ๐ฅ โ ๐ โฆ ๐ด ) ) = ( ๐ฅ โ ๐ โฆ ๐น ) ) |
36 |
35
|
feq1d |
โข ( ๐ โ ( ( ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) โ ( ๐ฅ โ ๐ โฆ ๐ด ) ) : ๐ โถ โ โ ( ๐ฅ โ ๐ โฆ ๐น ) : ๐ โถ โ ) ) |
37 |
34 36
|
mpbid |
โข ( ๐ โ ( ๐ฅ โ ๐ โฆ ๐น ) : ๐ โถ โ ) |
38 |
37
|
fvmptelcdm |
โข ( ( ๐ โง ๐ฅ โ ๐ ) โ ๐น โ โ ) |
39 |
30 38 4 35 7
|
offval2 |
โข ( ๐ โ ( ( ( ๐ D ( ๐ฆ โ ๐ โฆ ๐ถ ) ) โ ( ๐ฅ โ ๐ โฆ ๐ด ) ) โf ยท ( ๐ D ( ๐ฅ โ ๐ โฆ ๐ด ) ) ) = ( ๐ฅ โ ๐ โฆ ( ๐น ยท ๐ต ) ) ) |
40 |
23 27 39
|
3eqtr3d |
โข ( ๐ โ ( ๐ D ( ๐ฅ โ ๐ โฆ ๐ธ ) ) = ( ๐ฅ โ ๐ โฆ ( ๐น ยท ๐ต ) ) ) |