Step | Hyp | Ref
| Expression |
1 | | df-dv 25383 |
. . . . . . . . . . . . . . . . . . . 20
β’ D =
(π β π«
β, π β (β
βpm π )
β¦ βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯))) |
2 | 1 | dmmpossx 8051 |
. . . . . . . . . . . . . . . . . . 19
β’ dom D
β βͺ π β π« β({π } Γ (β βpm π )) |
3 | | simpl 483 |
. . . . . . . . . . . . . . . . . . 19
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
β¨π, πΉβ© β dom D ) |
4 | 2, 3 | sselid 3980 |
. . . . . . . . . . . . . . . . . 18
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
β¨π, πΉβ© β βͺ π β π« β({π } Γ (β βpm π ))) |
5 | | oveq2 7416 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (β βpm π ) = (β βpm
π)) |
6 | 5 | opeliunxp2 5838 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π, πΉβ© β βͺ π β π« β({π } Γ (β βpm π )) β (π β π« β β§ πΉ β (β
βpm π))) |
7 | 4, 6 | sylib 217 |
. . . . . . . . . . . . . . . . 17
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (π β π« β β§
πΉ β (β
βpm π))) |
8 | 7 | simprd 496 |
. . . . . . . . . . . . . . . 16
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β πΉ β (β
βpm π)) |
9 | | cnex 11190 |
. . . . . . . . . . . . . . . . 17
β’ β
β V |
10 | 7 | simpld 495 |
. . . . . . . . . . . . . . . . 17
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β π β π«
β) |
11 | | elpm2g 8837 |
. . . . . . . . . . . . . . . . 17
β’ ((β
β V β§ π β
π« β) β (πΉ β (β βpm π) β (πΉ:dom πΉβΆβ β§ dom πΉ β π))) |
12 | 9, 10, 11 | sylancr 587 |
. . . . . . . . . . . . . . . 16
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (πΉ β (β
βpm π)
β (πΉ:dom πΉβΆβ β§ dom πΉ β π))) |
13 | 8, 12 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (πΉ:dom πΉβΆβ β§ dom πΉ β π)) |
14 | 13 | simpld 495 |
. . . . . . . . . . . . . 14
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β πΉ:dom πΉβΆβ) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . 13
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β πΉ:dom πΉβΆβ) |
16 | 2 | sseli 3978 |
. . . . . . . . . . . . . . . . . . . 20
β’
(β¨π, πΉβ© β dom D β
β¨π, πΉβ© β βͺ π β π« β({π } Γ (β βpm π ))) |
17 | 16, 6 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨π, πΉβ© β dom D β
(π β π« β
β§ πΉ β (β
βpm π))) |
18 | 17 | simprd 496 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π, πΉβ© β dom D β πΉ β (β
βpm π)) |
19 | 17 | simpld 495 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨π, πΉβ© β dom D β π β π«
β) |
20 | 9, 19, 11 | sylancr 587 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π, πΉβ© β dom D β
(πΉ β (β
βpm π)
β (πΉ:dom πΉβΆβ β§ dom πΉ β π))) |
21 | 18, 20 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
β’
(β¨π, πΉβ© β dom D β
(πΉ:dom πΉβΆβ β§ dom πΉ β π)) |
22 | 21 | simprd 496 |
. . . . . . . . . . . . . . . 16
β’
(β¨π, πΉβ© β dom D β dom
πΉ β π) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . . 15
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β dom πΉ β π) |
24 | 10 | elpwid 4611 |
. . . . . . . . . . . . . . 15
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β π β
β) |
25 | 23, 24 | sstrd 3992 |
. . . . . . . . . . . . . 14
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β dom πΉ β
β) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . 13
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β dom πΉ β β) |
27 | | perfdvf.1 |
. . . . . . . . . . . . . . . . . 18
β’ πΎ =
(TopOpenββfld) |
28 | 27 | cnfldtopon 24298 |
. . . . . . . . . . . . . . . . 17
β’ πΎ β
(TopOnββ) |
29 | | resttopon 22664 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β (TopOnββ)
β§ π β β)
β (πΎ
βΎt π)
β (TopOnβπ)) |
30 | 28, 24, 29 | sylancr 587 |
. . . . . . . . . . . . . . . 16
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (πΎ βΎt π) β (TopOnβπ)) |
31 | | topontop 22414 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ βΎt π) β (TopOnβπ) β (πΎ βΎt π) β Top) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . 15
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (πΎ βΎt π) β Top) |
33 | | toponuni 22415 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ βΎt π) β (TopOnβπ) β π = βͺ (πΎ βΎt π)) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β π = βͺ
(πΎ βΎt
π)) |
35 | 23, 34 | sseqtrd 4022 |
. . . . . . . . . . . . . . 15
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β dom πΉ β βͺ (πΎ
βΎt π)) |
36 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
β’ βͺ (πΎ
βΎt π) =
βͺ (πΎ βΎt π) |
37 | 36 | ntrss2 22560 |
. . . . . . . . . . . . . . 15
β’ (((πΎ βΎt π) β Top β§ dom πΉ β βͺ (πΎ
βΎt π))
β ((intβ(πΎ
βΎt π))βdom πΉ) β dom πΉ) |
38 | 32, 35, 37 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
((intβ(πΎ
βΎt π))βdom πΉ) β dom πΉ) |
39 | 38 | sselda 3982 |
. . . . . . . . . . . . 13
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β π₯ β dom πΉ) |
40 | 15, 26, 39 | dvlem 25412 |
. . . . . . . . . . . 12
β’
((((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β§ π§ β (dom πΉ β {π₯})) β (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)) β β) |
41 | 40 | fmpttd 7114 |
. . . . . . . . . . 11
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β (π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))):(dom πΉ β {π₯})βΆβ) |
42 | 26 | ssdifssd 4142 |
. . . . . . . . . . 11
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β (dom πΉ β {π₯}) β β) |
43 | 36 | ntrss3 22563 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΎ βΎt π) β Top β§ dom πΉ β βͺ (πΎ
βΎt π))
β ((intβ(πΎ
βΎt π))βdom πΉ) β βͺ
(πΎ βΎt
π)) |
44 | 32, 35, 43 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
((intβ(πΎ
βΎt π))βdom πΉ) β βͺ
(πΎ βΎt
π)) |
45 | 44, 34 | sseqtrrd 4023 |
. . . . . . . . . . . . . . . . 17
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
((intβ(πΎ
βΎt π))βdom πΉ) β π) |
46 | | restabs 22668 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β (TopOnββ)
β§ ((intβ(πΎ
βΎt π))βdom πΉ) β π β§ π β π« β) β ((πΎ βΎt π) βΎt
((intβ(πΎ
βΎt π))βdom πΉ)) = (πΎ βΎt ((intβ(πΎ βΎt π))βdom πΉ))) |
47 | 28, 45, 10, 46 | mp3an2i 1466 |
. . . . . . . . . . . . . . . 16
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β ((πΎ βΎt π) βΎt
((intβ(πΎ
βΎt π))βdom πΉ)) = (πΎ βΎt ((intβ(πΎ βΎt π))βdom πΉ))) |
48 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (πΎ βΎt π) β Perf) |
49 | 36 | ntropn 22552 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΎ βΎt π) β Top β§ dom πΉ β βͺ (πΎ
βΎt π))
β ((intβ(πΎ
βΎt π))βdom πΉ) β (πΎ βΎt π)) |
50 | 32, 35, 49 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
((intβ(πΎ
βΎt π))βdom πΉ) β (πΎ βΎt π)) |
51 | | eqid 2732 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ βΎt π) βΎt
((intβ(πΎ
βΎt π))βdom πΉ)) = ((πΎ βΎt π) βΎt ((intβ(πΎ βΎt π))βdom πΉ)) |
52 | 36, 51 | perfopn 22688 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ βΎt π) β Perf β§
((intβ(πΎ
βΎt π))βdom πΉ) β (πΎ βΎt π)) β ((πΎ βΎt π) βΎt ((intβ(πΎ βΎt π))βdom πΉ)) β Perf) |
53 | 48, 50, 52 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β ((πΎ βΎt π) βΎt
((intβ(πΎ
βΎt π))βdom πΉ)) β Perf) |
54 | 47, 53 | eqeltrrd 2834 |
. . . . . . . . . . . . . . 15
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (πΎ βΎt
((intβ(πΎ
βΎt π))βdom πΉ)) β Perf) |
55 | 27 | cnfldtop 24299 |
. . . . . . . . . . . . . . . 16
β’ πΎ β Top |
56 | 45, 24 | sstrd 3992 |
. . . . . . . . . . . . . . . 16
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
((intβ(πΎ
βΎt π))βdom πΉ) β β) |
57 | 28 | toponunii 22417 |
. . . . . . . . . . . . . . . . 17
β’ β =
βͺ πΎ |
58 | | eqid 2732 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ βΎt
((intβ(πΎ
βΎt π))βdom πΉ)) = (πΎ βΎt ((intβ(πΎ βΎt π))βdom πΉ)) |
59 | 57, 58 | restperf 22687 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Top β§
((intβ(πΎ
βΎt π))βdom πΉ) β β) β ((πΎ βΎt
((intβ(πΎ
βΎt π))βdom πΉ)) β Perf β ((intβ(πΎ βΎt π))βdom πΉ) β ((limPtβπΎ)β((intβ(πΎ βΎt π))βdom πΉ)))) |
60 | 55, 56, 59 | sylancr 587 |
. . . . . . . . . . . . . . 15
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β ((πΎ βΎt
((intβ(πΎ
βΎt π))βdom πΉ)) β Perf β ((intβ(πΎ βΎt π))βdom πΉ) β ((limPtβπΎ)β((intβ(πΎ βΎt π))βdom πΉ)))) |
61 | 54, 60 | mpbid 231 |
. . . . . . . . . . . . . 14
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
((intβ(πΎ
βΎt π))βdom πΉ) β ((limPtβπΎ)β((intβ(πΎ βΎt π))βdom πΉ))) |
62 | 57 | lpss3 22647 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β Top β§ dom πΉ β β β§
((intβ(πΎ
βΎt π))βdom πΉ) β dom πΉ) β ((limPtβπΎ)β((intβ(πΎ βΎt π))βdom πΉ)) β ((limPtβπΎ)βdom πΉ)) |
63 | 55, 25, 38, 62 | mp3an2i 1466 |
. . . . . . . . . . . . . 14
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
((limPtβπΎ)β((intβ(πΎ βΎt π))βdom πΉ)) β ((limPtβπΎ)βdom πΉ)) |
64 | 61, 63 | sstrd 3992 |
. . . . . . . . . . . . 13
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
((intβ(πΎ
βΎt π))βdom πΉ) β ((limPtβπΎ)βdom πΉ)) |
65 | 64 | sselda 3982 |
. . . . . . . . . . . 12
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β π₯ β ((limPtβπΎ)βdom πΉ)) |
66 | 57 | lpdifsn 22646 |
. . . . . . . . . . . . 13
β’ ((πΎ β Top β§ dom πΉ β β) β (π₯ β ((limPtβπΎ)βdom πΉ) β π₯ β ((limPtβπΎ)β(dom πΉ β {π₯})))) |
67 | 55, 26, 66 | sylancr 587 |
. . . . . . . . . . . 12
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β (π₯ β ((limPtβπΎ)βdom πΉ) β π₯ β ((limPtβπΎ)β(dom πΉ β {π₯})))) |
68 | 65, 67 | mpbid 231 |
. . . . . . . . . . 11
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β π₯ β ((limPtβπΎ)β(dom πΉ β {π₯}))) |
69 | 41, 42, 68, 27 | limcmo 25398 |
. . . . . . . . . 10
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯ β ((intβ(πΎ βΎt π))βdom πΉ)) β β*π¦ π¦ β ((π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) |
70 | 69 | ex 413 |
. . . . . . . . 9
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (π₯ β ((intβ(πΎ βΎt π))βdom πΉ) β β*π¦ π¦ β ((π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
71 | | moanimv 2615 |
. . . . . . . . 9
β’
(β*π¦(π₯ β ((intβ(πΎ βΎt π))βdom πΉ) β§ π¦ β ((π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β (π₯ β ((intβ(πΎ βΎt π))βdom πΉ) β β*π¦ π¦ β ((π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
72 | 70, 71 | sylibr 233 |
. . . . . . . 8
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
β*π¦(π₯ β ((intβ(πΎ βΎt π))βdom πΉ) β§ π¦ β ((π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
73 | | eqid 2732 |
. . . . . . . . . 10
β’ (πΎ βΎt π) = (πΎ βΎt π) |
74 | | eqid 2732 |
. . . . . . . . . 10
β’ (π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = (π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
75 | 73, 27, 74, 24, 14, 23 | eldv 25414 |
. . . . . . . . 9
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (π₯(π D πΉ)π¦ β (π₯ β ((intβ(πΎ βΎt π))βdom πΉ) β§ π¦ β ((π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)))) |
76 | 75 | mobidv 2543 |
. . . . . . . 8
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
(β*π¦ π₯(π D πΉ)π¦ β β*π¦(π₯ β ((intβ(πΎ βΎt π))βdom πΉ) β§ π¦ β ((π§ β (dom πΉ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)))) |
77 | 72, 76 | mpbird 256 |
. . . . . . 7
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
β*π¦ π₯(π D πΉ)π¦) |
78 | 77 | alrimiv 1930 |
. . . . . 6
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
βπ₯β*π¦ π₯(π D πΉ)π¦) |
79 | | reldv 25386 |
. . . . . . 7
β’ Rel
(π D πΉ) |
80 | | dffun6 6556 |
. . . . . . 7
β’ (Fun
(π D πΉ) β (Rel (π D πΉ) β§ βπ₯β*π¦ π₯(π D πΉ)π¦)) |
81 | 79, 80 | mpbiran 707 |
. . . . . 6
β’ (Fun
(π D πΉ) β βπ₯β*π¦ π₯(π D πΉ)π¦) |
82 | 78, 81 | sylibr 233 |
. . . . 5
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β Fun (π D πΉ)) |
83 | 82 | funfnd 6579 |
. . . 4
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (π D πΉ) Fn dom (π D πΉ)) |
84 | | vex 3478 |
. . . . . . 7
β’ π¦ β V |
85 | 84 | elrn 5893 |
. . . . . 6
β’ (π¦ β ran (π D πΉ) β βπ₯ π₯(π D πΉ)π¦) |
86 | 24, 14, 23 | dvcl 25415 |
. . . . . . . 8
β’
(((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β§ π₯(π D πΉ)π¦) β π¦ β β) |
87 | 86 | ex 413 |
. . . . . . 7
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (π₯(π D πΉ)π¦ β π¦ β β)) |
88 | 87 | exlimdv 1936 |
. . . . . 6
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β
(βπ₯ π₯(π D πΉ)π¦ β π¦ β β)) |
89 | 85, 88 | biimtrid 241 |
. . . . 5
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (π¦ β ran (π D πΉ) β π¦ β β)) |
90 | 89 | ssrdv 3988 |
. . . 4
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β ran (π D πΉ) β β) |
91 | | df-f 6547 |
. . . 4
β’ ((π D πΉ):dom (π D πΉ)βΆβ β ((π D πΉ) Fn dom (π D πΉ) β§ ran (π D πΉ) β β)) |
92 | 83, 90, 91 | sylanbrc 583 |
. . 3
β’
((β¨π, πΉβ© β dom D β§ (πΎ βΎt π) β Perf) β (π D πΉ):dom (π D πΉ)βΆβ) |
93 | 92 | ex 413 |
. 2
β’
(β¨π, πΉβ© β dom D β
((πΎ βΎt
π) β Perf β
(π D πΉ):dom (π D πΉ)βΆβ)) |
94 | | f0 6772 |
. . . 4
β’
β
:β
βΆβ |
95 | | df-ov 7411 |
. . . . . 6
β’ (π D πΉ) = ( D ββ¨π, πΉβ©) |
96 | | ndmfv 6926 |
. . . . . 6
β’ (Β¬
β¨π, πΉβ© β dom D β ( D
ββ¨π, πΉβ©) =
β
) |
97 | 95, 96 | eqtrid 2784 |
. . . . 5
β’ (Β¬
β¨π, πΉβ© β dom D β (π D πΉ) = β
) |
98 | 97 | dmeqd 5905 |
. . . . . 6
β’ (Β¬
β¨π, πΉβ© β dom D β dom (π D πΉ) = dom β
) |
99 | | dm0 5920 |
. . . . . 6
β’ dom
β
= β
|
100 | 98, 99 | eqtrdi 2788 |
. . . . 5
β’ (Β¬
β¨π, πΉβ© β dom D β dom (π D πΉ) = β
) |
101 | 97, 100 | feq12d 6705 |
. . . 4
β’ (Β¬
β¨π, πΉβ© β dom D β ((π D πΉ):dom (π D πΉ)βΆβ β
β
:β
βΆβ)) |
102 | 94, 101 | mpbiri 257 |
. . 3
β’ (Β¬
β¨π, πΉβ© β dom D β (π D πΉ):dom (π D πΉ)βΆβ) |
103 | 102 | a1d 25 |
. 2
β’ (Β¬
β¨π, πΉβ© β dom D β ((πΎ βΎt π) β Perf β (π D πΉ):dom (π D πΉ)βΆβ)) |
104 | 93, 103 | pm2.61i 182 |
1
β’ ((πΎ βΎt π) β Perf β (π D πΉ):dom (π D πΉ)βΆβ) |