Step | Hyp | Ref
| Expression |
1 | | df-dv 25254 |
. . . . . . . . . . 11
β’ D =
(π β π«
β, π β (β
βpm π )
β¦ βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯))) |
2 | 1 | reldmmpo 7494 |
. . . . . . . . . 10
β’ Rel dom
D |
3 | | df-rel 5644 |
. . . . . . . . . 10
β’ (Rel dom
D β dom D β (V Γ V)) |
4 | 2, 3 | mpbi 229 |
. . . . . . . . 9
β’ dom D
β (V Γ V) |
5 | 4 | sseli 3944 |
. . . . . . . 8
β’
(β¨π, πΉβ© β dom D β
β¨π, πΉβ© β (V Γ
V)) |
6 | | opelxp1 5678 |
. . . . . . . 8
β’
(β¨π, πΉβ© β (V Γ V)
β π β
V) |
7 | 5, 6 | syl 17 |
. . . . . . 7
β’
(β¨π, πΉβ© β dom D β π β V) |
8 | | opeq1 4834 |
. . . . . . . . . 10
β’ (π = π β β¨π , πΉβ© = β¨π, πΉβ©) |
9 | 8 | eleq1d 2819 |
. . . . . . . . 9
β’ (π = π β (β¨π , πΉβ© β dom D β β¨π, πΉβ© β dom D )) |
10 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = π β (π β π« β β π β π«
β)) |
11 | | oveq2 7369 |
. . . . . . . . . . 11
β’ (π = π β (β βpm π ) = (β βpm
π)) |
12 | 11 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π = π β (πΉ β (β βpm π ) β πΉ β (β βpm π))) |
13 | 10, 12 | anbi12d 632 |
. . . . . . . . 9
β’ (π = π β ((π β π« β β§ πΉ β (β
βpm π ))
β (π β π«
β β§ πΉ β
(β βpm π)))) |
14 | 9, 13 | imbi12d 345 |
. . . . . . . 8
β’ (π = π β ((β¨π , πΉβ© β dom D β (π β π« β β§
πΉ β (β
βpm π )))
β (β¨π, πΉβ© β dom D β
(π β π« β
β§ πΉ β (β
βpm π))))) |
15 | 1 | dmmpossx 8002 |
. . . . . . . . . 10
β’ dom D
β βͺ π β π« β({π } Γ (β βpm π )) |
16 | 15 | sseli 3944 |
. . . . . . . . 9
β’
(β¨π , πΉβ© β dom D β
β¨π , πΉβ© β βͺ π β π« β({π } Γ (β βpm π ))) |
17 | | opeliunxp 5703 |
. . . . . . . . 9
β’
(β¨π , πΉβ© β βͺ π β π« β({π } Γ (β βpm π )) β (π β π« β β§ πΉ β (β
βpm π ))) |
18 | 16, 17 | sylib 217 |
. . . . . . . 8
β’
(β¨π , πΉβ© β dom D β
(π β π« β
β§ πΉ β (β
βpm π ))) |
19 | 14, 18 | vtoclg 3527 |
. . . . . . 7
β’ (π β V β (β¨π, πΉβ© β dom D β (π β π« β β§
πΉ β (β
βpm π)))) |
20 | 7, 19 | mpcom 38 |
. . . . . 6
β’
(β¨π, πΉβ© β dom D β
(π β π« β
β§ πΉ β (β
βpm π))) |
21 | 20 | simpld 496 |
. . . . 5
β’
(β¨π, πΉβ© β dom D β π β π«
β) |
22 | 21 | elpwid 4573 |
. . . 4
β’
(β¨π, πΉβ© β dom D β π β
β) |
23 | 20 | simprd 497 |
. . . . . 6
β’
(β¨π, πΉβ© β dom D β πΉ β (β
βpm π)) |
24 | | cnex 11140 |
. . . . . . 7
β’ β
β V |
25 | | elpm2g 8788 |
. . . . . . 7
β’ ((β
β V β§ π β
π« β) β (πΉ β (β βpm π) β (πΉ:dom πΉβΆβ β§ dom πΉ β π))) |
26 | 24, 21, 25 | sylancr 588 |
. . . . . 6
β’
(β¨π, πΉβ© β dom D β
(πΉ β (β
βpm π)
β (πΉ:dom πΉβΆβ β§ dom πΉ β π))) |
27 | 23, 26 | mpbid 231 |
. . . . 5
β’
(β¨π, πΉβ© β dom D β
(πΉ:dom πΉβΆβ β§ dom πΉ β π)) |
28 | 27 | simpld 496 |
. . . 4
β’
(β¨π, πΉβ© β dom D β πΉ:dom πΉβΆβ) |
29 | 27 | simprd 497 |
. . . 4
β’
(β¨π, πΉβ© β dom D β dom
πΉ β π) |
30 | 22, 28, 29 | dvbss 25288 |
. . 3
β’
(β¨π, πΉβ© β dom D β dom
(π D πΉ) β dom πΉ) |
31 | 30, 29 | sstrd 3958 |
. 2
β’
(β¨π, πΉβ© β dom D β dom
(π D πΉ) β π) |
32 | | df-ov 7364 |
. . . . . 6
β’ (π D πΉ) = ( D ββ¨π, πΉβ©) |
33 | | ndmfv 6881 |
. . . . . 6
β’ (Β¬
β¨π, πΉβ© β dom D β ( D
ββ¨π, πΉβ©) =
β
) |
34 | 32, 33 | eqtrid 2785 |
. . . . 5
β’ (Β¬
β¨π, πΉβ© β dom D β (π D πΉ) = β
) |
35 | 34 | dmeqd 5865 |
. . . 4
β’ (Β¬
β¨π, πΉβ© β dom D β dom (π D πΉ) = dom β
) |
36 | | dm0 5880 |
. . . 4
β’ dom
β
= β
|
37 | 35, 36 | eqtrdi 2789 |
. . 3
β’ (Β¬
β¨π, πΉβ© β dom D β dom (π D πΉ) = β
) |
38 | | 0ss 4360 |
. . 3
β’ β
β π |
39 | 37, 38 | eqsstrdi 4002 |
. 2
β’ (Β¬
β¨π, πΉβ© β dom D β dom (π D πΉ) β π) |
40 | 31, 39 | pm2.61i 182 |
1
β’ dom
(π D πΉ) β π |