Step | Hyp | Ref
| Expression |
1 | | relxp 5695 |
. . . . . . . 8
β’ Rel
({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) |
2 | 1 | rgenw 3066 |
. . . . . . 7
β’
βπ₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)Rel ({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) |
3 | | reliun 5817 |
. . . . . . 7
β’ (Rel
βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) β βπ₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)Rel ({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯))) |
4 | 2, 3 | mpbir 230 |
. . . . . 6
β’ Rel
βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) |
5 | | df-rel 5684 |
. . . . . 6
β’ (Rel
βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) β βͺ
π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) β (V Γ V)) |
6 | 4, 5 | mpbi 229 |
. . . . 5
β’ βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) β (V Γ V) |
7 | 6 | rgenw 3066 |
. . . 4
β’
βπ β
(β βpm π )βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) β (V Γ V) |
8 | 7 | rgenw 3066 |
. . 3
β’
βπ β
π« ββπ
β (β βpm π )βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) β (V Γ V) |
9 | | df-dv 25384 |
. . . 4
β’ D =
(π β π«
β, π β (β
βpm π )
β¦ βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯))) |
10 | 9 | ovmptss 8079 |
. . 3
β’
(βπ β
π« ββπ
β (β βpm π )βͺ π₯ β
((intβ((TopOpenββfld) βΎt π ))βdom π)({π₯} Γ ((π§ β (dom π β {π₯}) β¦ (((πβπ§) β (πβπ₯)) / (π§ β π₯))) limβ π₯)) β (V Γ V) β (π D πΉ) β (V Γ V)) |
11 | 8, 10 | ax-mp 5 |
. 2
β’ (π D πΉ) β (V Γ V) |
12 | | df-rel 5684 |
. 2
β’ (Rel
(π D πΉ) β (π D πΉ) β (V Γ V)) |
13 | 11, 12 | mpbir 230 |
1
β’ Rel
(π D πΉ) |