Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . . . 5
β’ ((π β β β§ πΉ β (β
βpm π)) β π β β) |
2 | | cnex 7934 |
. . . . . 6
β’ β
β V |
3 | 2 | elpw2 4157 |
. . . . 5
β’ (π β π« β β
π β
β) |
4 | 1, 3 | sylibr 134 |
. . . 4
β’ ((π β β β§ πΉ β (β
βpm π)) β π β π« β) |
5 | | simpr 110 |
. . . 4
β’ ((π β β β§ πΉ β (β
βpm π)) β πΉ β (β βpm
π)) |
6 | | eqid 2177 |
. . . . . . . . . 10
β’
(MetOpenβ(abs β β )) = (MetOpenβ(abs β
β )) |
7 | 6 | cntoptop 13969 |
. . . . . . . . 9
β’
(MetOpenβ(abs β β )) β Top |
8 | 7 | a1i 9 |
. . . . . . . 8
β’ ((π β β β§ πΉ β (β
βpm π)) β (MetOpenβ(abs β
β )) β Top) |
9 | 4 | elexd 2750 |
. . . . . . . 8
β’ ((π β β β§ πΉ β (β
βpm π)) β π β V) |
10 | | resttop 13606 |
. . . . . . . 8
β’
(((MetOpenβ(abs β β )) β Top β§ π β V) β
((MetOpenβ(abs β β )) βΎt π) β Top) |
11 | 8, 9, 10 | syl2anc 411 |
. . . . . . 7
β’ ((π β β β§ πΉ β (β
βpm π)) β ((MetOpenβ(abs β
β )) βΎt π) β Top) |
12 | | elpmi 6666 |
. . . . . . . . . 10
β’ (πΉ β (β
βpm π) β (πΉ:dom πΉβΆβ β§ dom πΉ β π)) |
13 | 12 | simprd 114 |
. . . . . . . . 9
β’ (πΉ β (β
βpm π) β dom πΉ β π) |
14 | 13 | adantl 277 |
. . . . . . . 8
β’ ((π β β β§ πΉ β (β
βpm π)) β dom πΉ β π) |
15 | 6 | cntoptopon 13968 |
. . . . . . . . . . 11
β’
(MetOpenβ(abs β β )) β
(TopOnββ) |
16 | 15 | toponunii 13453 |
. . . . . . . . . 10
β’ β =
βͺ (MetOpenβ(abs β β
)) |
17 | 16 | restuni 13608 |
. . . . . . . . 9
β’
(((MetOpenβ(abs β β )) β Top β§ π β β) β π = βͺ
((MetOpenβ(abs β β )) βΎt π)) |
18 | 8, 1, 17 | syl2anc 411 |
. . . . . . . 8
β’ ((π β β β§ πΉ β (β
βpm π)) β π = βͺ
((MetOpenβ(abs β β )) βΎt π)) |
19 | 14, 18 | sseqtrd 3193 |
. . . . . . 7
β’ ((π β β β§ πΉ β (β
βpm π)) β dom πΉ β βͺ
((MetOpenβ(abs β β )) βΎt π)) |
20 | | eqid 2177 |
. . . . . . . 8
β’ βͺ ((MetOpenβ(abs β β ))
βΎt π) =
βͺ ((MetOpenβ(abs β β ))
βΎt π) |
21 | 20 | ntrss3 13559 |
. . . . . . 7
β’
((((MetOpenβ(abs β β )) βΎt π) β Top β§ dom πΉ β βͺ ((MetOpenβ(abs β β ))
βΎt π))
β ((intβ((MetOpenβ(abs β β )) βΎt
π))βdom πΉ) β βͺ ((MetOpenβ(abs β β ))
βΎt π)) |
22 | 11, 19, 21 | syl2anc 411 |
. . . . . 6
β’ ((π β β β§ πΉ β (β
βpm π)) β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β βͺ
((MetOpenβ(abs β β )) βΎt π)) |
23 | | uniexg 4439 |
. . . . . . 7
β’
(((MetOpenβ(abs β β )) βΎt π) β Top β βͺ ((MetOpenβ(abs β β ))
βΎt π)
β V) |
24 | | elpw2g 4156 |
. . . . . . 7
β’ (βͺ ((MetOpenβ(abs β β ))
βΎt π)
β V β (((intβ((MetOpenβ(abs β β ))
βΎt π))βdom πΉ) β π« βͺ ((MetOpenβ(abs β β ))
βΎt π)
β ((intβ((MetOpenβ(abs β β )) βΎt
π))βdom πΉ) β βͺ ((MetOpenβ(abs β β ))
βΎt π))) |
25 | 11, 23, 24 | 3syl 17 |
. . . . . 6
β’ ((π β β β§ πΉ β (β
βpm π)) β (((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β π« βͺ ((MetOpenβ(abs β β ))
βΎt π)
β ((intβ((MetOpenβ(abs β β )) βΎt
π))βdom πΉ) β βͺ ((MetOpenβ(abs β β ))
βΎt π))) |
26 | 22, 25 | mpbird 167 |
. . . . 5
β’ ((π β β β§ πΉ β (β
βpm π)) β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ) β π« βͺ ((MetOpenβ(abs β β ))
βΎt π)) |
27 | | vex 2740 |
. . . . . . . . 9
β’ π₯ β V |
28 | 27 | snex 4185 |
. . . . . . . 8
β’ {π₯} β V |
29 | | limccl 14064 |
. . . . . . . . 9
β’ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯) β β |
30 | 2, 29 | ssexi 4141 |
. . . . . . . 8
β’ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯) β V |
31 | 28, 30 | xpex 4741 |
. . . . . . 7
β’ ({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β V |
32 | 31 | rgenw 2532 |
. . . . . 6
β’
βπ₯ β
((intβ((MetOpenβ(abs β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β V |
33 | 32 | a1i 9 |
. . . . 5
β’ ((π β β β§ πΉ β (β
βpm π)) β βπ₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β V) |
34 | | iunexg 6119 |
. . . . 5
β’
((((intβ((MetOpenβ(abs β β ))
βΎt π))βdom πΉ) β π« βͺ ((MetOpenβ(abs β β ))
βΎt π)
β§ βπ₯ β
((intβ((MetOpenβ(abs β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β V) β βͺ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β V) |
35 | 26, 33, 34 | syl2anc 411 |
. . . 4
β’ ((π β β β§ πΉ β (β
βpm π)) β βͺ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β V) |
36 | | simpl 109 |
. . . . . . . . 9
β’ ((π = π β§ π = πΉ) β π = π) |
37 | 36 | oveq2d 5890 |
. . . . . . . 8
β’ ((π = π β§ π = πΉ) β ((MetOpenβ(abs β
β )) βΎt π ) = ((MetOpenβ(abs β β ))
βΎt π)) |
38 | 37 | fveq2d 5519 |
. . . . . . 7
β’ ((π = π β§ π = πΉ) β (intβ((MetOpenβ(abs
β β )) βΎt π )) = (intβ((MetOpenβ(abs β
β )) βΎt π))) |
39 | | dmeq 4827 |
. . . . . . . 8
β’ (π = πΉ β dom π = dom πΉ) |
40 | 39 | adantl 277 |
. . . . . . 7
β’ ((π = π β§ π = πΉ) β dom π = dom πΉ) |
41 | 38, 40 | fveq12d 5522 |
. . . . . 6
β’ ((π = π β§ π = πΉ) β ((intβ((MetOpenβ(abs
β β )) βΎt π ))βdom π) = ((intβ((MetOpenβ(abs β
β )) βΎt π))βdom πΉ)) |
42 | 40 | rabeqdv 2731 |
. . . . . . . . 9
β’ ((π = π β§ π = πΉ) β {π€ β dom π β£ π€ # π₯} = {π€ β dom πΉ β£ π€ # π₯}) |
43 | | fveq1 5514 |
. . . . . . . . . . . 12
β’ (π = πΉ β (πβπ§) = (πΉβπ§)) |
44 | 43 | adantl 277 |
. . . . . . . . . . 11
β’ ((π = π β§ π = πΉ) β (πβπ§) = (πΉβπ§)) |
45 | | fveq1 5514 |
. . . . . . . . . . . 12
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
46 | 45 | adantl 277 |
. . . . . . . . . . 11
β’ ((π = π β§ π = πΉ) β (πβπ₯) = (πΉβπ₯)) |
47 | 44, 46 | oveq12d 5892 |
. . . . . . . . . 10
β’ ((π = π β§ π = πΉ) β ((πβπ§) β (πβπ₯)) = ((πΉβπ§) β (πΉβπ₯))) |
48 | 47 | oveq1d 5889 |
. . . . . . . . 9
β’ ((π = π β§ π = πΉ) β (((πβπ§) β (πβπ₯)) / (π§ β π₯)) = (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
49 | 42, 48 | mpteq12dv 4085 |
. . . . . . . 8
β’ ((π = π β§ π = πΉ) β (π§ β {π€ β dom π β£ π€ # π₯} β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) = (π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯)))) |
50 | 49 | oveq1d 5889 |
. . . . . . 7
β’ ((π = π β§ π = πΉ) β ((π§ β {π€ β dom π β£ π€ # π₯} β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯) = ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) |
51 | 50 | xpeq2d 4650 |
. . . . . 6
β’ ((π = π β§ π = πΉ) β ({π₯} Γ ((π§ β {π€ β dom π β£ π€ # π₯} β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) = ({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
52 | 41, 51 | iuneq12d 3910 |
. . . . 5
β’ ((π = π β§ π = πΉ) β βͺ
π₯ β
((intβ((MetOpenβ(abs β β )) βΎt π ))βdom π)({π₯} Γ ((π§ β {π€ β dom π β£ π€ # π₯} β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) = βͺ
π₯ β
((intβ((MetOpenβ(abs β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
53 | | oveq2 5882 |
. . . . 5
β’ (π = π β (β βpm
π ) = (β
βpm π)) |
54 | | df-dvap 14062 |
. . . . 5
β’ D =
(π β π«
β, π β (β
βpm π ) β¦ βͺ
π₯ β
((intβ((MetOpenβ(abs β β )) βΎt π ))βdom π)({π₯} Γ ((π§ β {π€ β dom π β£ π€ # π₯} β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯))) |
55 | 52, 53, 54 | ovmpox 6002 |
. . . 4
β’ ((π β π« β β§
πΉ β (β
βpm π) β§ βͺ
π₯ β
((intβ((MetOpenβ(abs β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β V) β (π D πΉ) = βͺ
π₯ β
((intβ((MetOpenβ(abs β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
56 | 4, 5, 35, 55 | syl3anc 1238 |
. . 3
β’ ((π β β β§ πΉ β (β
βpm π)) β (π D πΉ) = βͺ
π₯ β
((intβ((MetOpenβ(abs β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
57 | | relxp 4735 |
. . . . . 6
β’ Rel
({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) |
58 | 57 | rgenw 2532 |
. . . . 5
β’
βπ₯ β
((intβ((MetOpenβ(abs β β )) βΎt π))βdom πΉ)Rel ({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) |
59 | | reliun 4747 |
. . . . 5
β’ (Rel
βͺ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β βπ₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)Rel ({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯))) |
60 | 58, 59 | mpbir 146 |
. . . 4
β’ Rel
βͺ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) |
61 | | df-rel 4633 |
. . . 4
β’ (Rel
βͺ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β βͺ
π₯ β
((intβ((MetOpenβ(abs β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β (V Γ V)) |
62 | 60, 61 | mpbi 145 |
. . 3
β’ βͺ π₯ β ((intβ((MetOpenβ(abs
β β )) βΎt π))βdom πΉ)({π₯} Γ ((π§ β {π€ β dom πΉ β£ π€ # π₯} β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) limβ π₯)) β (V Γ V) |
63 | 56, 62 | eqsstrdi 3207 |
. 2
β’ ((π β β β§ πΉ β (β
βpm π)) β (π D πΉ) β (V Γ V)) |
64 | | df-rel 4633 |
. 2
β’ (Rel
(π D πΉ) β (π D πΉ) β (V Γ V)) |
65 | 63, 64 | sylibr 134 |
1
β’ ((π β β β§ πΉ β (β
βpm π)) β Rel (π D πΉ)) |