Step | Hyp | Ref
| Expression |
1 | | dvle.r |
. . . 4
β’ (π₯ = π β π΄ = π
) |
2 | 1 | eleq1d 2819 |
. . 3
β’ (π₯ = π β (π΄ β β β π
β β)) |
3 | | dvle.a |
. . . . 5
β’ (π β (π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ)) |
4 | | cncff 24272 |
. . . . 5
β’ ((π₯ β (π[,]π) β¦ π΄) β ((π[,]π)βcnββ) β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
6 | | eqid 2733 |
. . . . 5
β’ (π₯ β (π[,]π) β¦ π΄) = (π₯ β (π[,]π) β¦ π΄) |
7 | 6 | fmpt 7059 |
. . . 4
β’
(βπ₯ β
(π[,]π)π΄ β β β (π₯ β (π[,]π) β¦ π΄):(π[,]π)βΆβ) |
8 | 5, 7 | sylibr 233 |
. . 3
β’ (π β βπ₯ β (π[,]π)π΄ β β) |
9 | | dvle.y |
. . 3
β’ (π β π β (π[,]π)) |
10 | 2, 8, 9 | rspcdva 3581 |
. 2
β’ (π β π
β β) |
11 | | dvle.s |
. . . . 5
β’ (π₯ = π β πΆ = π) |
12 | 11 | eleq1d 2819 |
. . . 4
β’ (π₯ = π β (πΆ β β β π β β)) |
13 | | dvle.c |
. . . . . 6
β’ (π β (π₯ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ)) |
14 | | cncff 24272 |
. . . . . 6
β’ ((π₯ β (π[,]π) β¦ πΆ) β ((π[,]π)βcnββ) β (π₯ β (π[,]π) β¦ πΆ):(π[,]π)βΆβ) |
15 | 13, 14 | syl 17 |
. . . . 5
β’ (π β (π₯ β (π[,]π) β¦ πΆ):(π[,]π)βΆβ) |
16 | | eqid 2733 |
. . . . . 6
β’ (π₯ β (π[,]π) β¦ πΆ) = (π₯ β (π[,]π) β¦ πΆ) |
17 | 16 | fmpt 7059 |
. . . . 5
β’
(βπ₯ β
(π[,]π)πΆ β β β (π₯ β (π[,]π) β¦ πΆ):(π[,]π)βΆβ) |
18 | 15, 17 | sylibr 233 |
. . . 4
β’ (π β βπ₯ β (π[,]π)πΆ β β) |
19 | 12, 18, 9 | rspcdva 3581 |
. . 3
β’ (π β π β β) |
20 | | dvle.q |
. . . . 5
β’ (π₯ = π β πΆ = π) |
21 | 20 | eleq1d 2819 |
. . . 4
β’ (π₯ = π β (πΆ β β β π β β)) |
22 | | dvle.x |
. . . 4
β’ (π β π β (π[,]π)) |
23 | 21, 18, 22 | rspcdva 3581 |
. . 3
β’ (π β π β β) |
24 | 19, 23 | resubcld 11588 |
. 2
β’ (π β (π β π) β β) |
25 | | dvle.p |
. . . 4
β’ (π₯ = π β π΄ = π) |
26 | 25 | eleq1d 2819 |
. . 3
β’ (π₯ = π β (π΄ β β β π β β)) |
27 | 26, 8, 22 | rspcdva 3581 |
. 2
β’ (π β π β β) |
28 | 10 | recnd 11188 |
. . . . 5
β’ (π β π
β β) |
29 | 23 | recnd 11188 |
. . . . . 6
β’ (π β π β β) |
30 | 19 | recnd 11188 |
. . . . . 6
β’ (π β π β β) |
31 | 29, 30 | subcld 11517 |
. . . . 5
β’ (π β (π β π) β β) |
32 | 28, 31 | addcomd 11362 |
. . . 4
β’ (π β (π
+ (π β π)) = ((π β π) + π
)) |
33 | 28, 30, 29 | subsub2d 11546 |
. . . 4
β’ (π β (π
β (π β π)) = (π
+ (π β π))) |
34 | 29, 30, 28 | subsubd 11545 |
. . . 4
β’ (π β (π β (π β π
)) = ((π β π) + π
)) |
35 | 32, 33, 34 | 3eqtr4d 2783 |
. . 3
β’ (π β (π
β (π β π)) = (π β (π β π
))) |
36 | 19, 10 | resubcld 11588 |
. . . 4
β’ (π β (π β π
) β β) |
37 | | dvle.m |
. . . . . 6
β’ (π β π β β) |
38 | | dvle.n |
. . . . . 6
β’ (π β π β β) |
39 | | eqid 2733 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
40 | 39 | subcn 24245 |
. . . . . . 7
β’ β
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
41 | | ax-resscn 11113 |
. . . . . . 7
β’ β
β β |
42 | | resubcl 11470 |
. . . . . . 7
β’ ((πΆ β β β§ π΄ β β) β (πΆ β π΄) β β) |
43 | 39, 40, 13, 3, 41, 42 | cncfmpt2ss 24295 |
. . . . . 6
β’ (π β (π₯ β (π[,]π) β¦ (πΆ β π΄)) β ((π[,]π)βcnββ)) |
44 | 41 | a1i 11 |
. . . . . . . . 9
β’ (π β β β
β) |
45 | | iccssre 13352 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (π[,]π) β β) |
46 | 37, 38, 45 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π[,]π) β β) |
47 | 15 | fvmptelcdm 7062 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π[,]π)) β πΆ β β) |
48 | 5 | fvmptelcdm 7062 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π[,]π)) β π΄ β β) |
49 | 47, 48 | resubcld 11588 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π[,]π)) β (πΆ β π΄) β β) |
50 | 49 | recnd 11188 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π[,]π)) β (πΆ β π΄) β β) |
51 | 39 | tgioo2 24182 |
. . . . . . . . 9
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
52 | | iccntr 24200 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β
((intβ(topGenβran (,)))β(π[,]π)) = (π(,)π)) |
53 | 37, 38, 52 | syl2anc 585 |
. . . . . . . . 9
β’ (π β
((intβ(topGenβran (,)))β(π[,]π)) = (π(,)π)) |
54 | 44, 46, 50, 51, 39, 53 | dvmptntr 25351 |
. . . . . . . 8
β’ (π β (β D (π₯ β (π[,]π) β¦ (πΆ β π΄))) = (β D (π₯ β (π(,)π) β¦ (πΆ β π΄)))) |
55 | | reelprrecn 11148 |
. . . . . . . . . 10
β’ β
β {β, β} |
56 | 55 | a1i 11 |
. . . . . . . . 9
β’ (π β β β {β,
β}) |
57 | | ioossicc 13356 |
. . . . . . . . . . 11
β’ (π(,)π) β (π[,]π) |
58 | 57 | sseli 3941 |
. . . . . . . . . 10
β’ (π₯ β (π(,)π) β π₯ β (π[,]π)) |
59 | 47 | recnd 11188 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π[,]π)) β πΆ β β) |
60 | 58, 59 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(,)π)) β πΆ β β) |
61 | | dvle.f |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π(,)π)) β π΅ β€ π·) |
62 | | lerel 11224 |
. . . . . . . . . . 11
β’ Rel
β€ |
63 | 62 | brrelex2i 5690 |
. . . . . . . . . 10
β’ (π΅ β€ π· β π· β V) |
64 | 61, 63 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(,)π)) β π· β V) |
65 | | dvle.d |
. . . . . . . . 9
β’ (π β (β D (π₯ β (π(,)π) β¦ πΆ)) = (π₯ β (π(,)π) β¦ π·)) |
66 | 48 | recnd 11188 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π[,]π)) β π΄ β β) |
67 | 58, 66 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(,)π)) β π΄ β β) |
68 | 62 | brrelex1i 5689 |
. . . . . . . . . 10
β’ (π΅ β€ π· β π΅ β V) |
69 | 61, 68 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(,)π)) β π΅ β V) |
70 | | dvle.b |
. . . . . . . . 9
β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)) = (π₯ β (π(,)π) β¦ π΅)) |
71 | 56, 60, 64, 65, 67, 69, 70 | dvmptsub 25347 |
. . . . . . . 8
β’ (π β (β D (π₯ β (π(,)π) β¦ (πΆ β π΄))) = (π₯ β (π(,)π) β¦ (π· β π΅))) |
72 | 54, 71 | eqtrd 2773 |
. . . . . . 7
β’ (π β (β D (π₯ β (π[,]π) β¦ (πΆ β π΄))) = (π₯ β (π(,)π) β¦ (π· β π΅))) |
73 | 58, 47 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π(,)π)) β πΆ β β) |
74 | 73 | fmpttd 7064 |
. . . . . . . . . . . 12
β’ (π β (π₯ β (π(,)π) β¦ πΆ):(π(,)π)βΆβ) |
75 | | ioossre 13331 |
. . . . . . . . . . . 12
β’ (π(,)π) β β |
76 | | dvfre 25331 |
. . . . . . . . . . . 12
β’ (((π₯ β (π(,)π) β¦ πΆ):(π(,)π)βΆβ β§ (π(,)π) β β) β (β D (π₯ β (π(,)π) β¦ πΆ)):dom (β D (π₯ β (π(,)π) β¦ πΆ))βΆβ) |
77 | 74, 75, 76 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π(,)π) β¦ πΆ)):dom (β D (π₯ β (π(,)π) β¦ πΆ))βΆβ) |
78 | 65 | dmeqd 5862 |
. . . . . . . . . . . . 13
β’ (π β dom (β D (π₯ β (π(,)π) β¦ πΆ)) = dom (π₯ β (π(,)π) β¦ π·)) |
79 | 64 | ralrimiva 3140 |
. . . . . . . . . . . . . 14
β’ (π β βπ₯ β (π(,)π)π· β V) |
80 | | dmmptg 6195 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
(π(,)π)π· β V β dom (π₯ β (π(,)π) β¦ π·) = (π(,)π)) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β dom (π₯ β (π(,)π) β¦ π·) = (π(,)π)) |
82 | 78, 81 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β dom (β D (π₯ β (π(,)π) β¦ πΆ)) = (π(,)π)) |
83 | 65, 82 | feq12d 6657 |
. . . . . . . . . . 11
β’ (π β ((β D (π₯ β (π(,)π) β¦ πΆ)):dom (β D (π₯ β (π(,)π) β¦ πΆ))βΆβ β (π₯ β (π(,)π) β¦ π·):(π(,)π)βΆβ)) |
84 | 77, 83 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (π₯ β (π(,)π) β¦ π·):(π(,)π)βΆβ) |
85 | 84 | fvmptelcdm 7062 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(,)π)) β π· β β) |
86 | 58, 48 | sylan2 594 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β (π(,)π)) β π΄ β β) |
87 | 86 | fmpttd 7064 |
. . . . . . . . . . . 12
β’ (π β (π₯ β (π(,)π) β¦ π΄):(π(,)π)βΆβ) |
88 | | dvfre 25331 |
. . . . . . . . . . . 12
β’ (((π₯ β (π(,)π) β¦ π΄):(π(,)π)βΆβ β§ (π(,)π) β β) β (β D (π₯ β (π(,)π) β¦ π΄)):dom (β D (π₯ β (π(,)π) β¦ π΄))βΆβ) |
89 | 87, 75, 88 | sylancl 587 |
. . . . . . . . . . 11
β’ (π β (β D (π₯ β (π(,)π) β¦ π΄)):dom (β D (π₯ β (π(,)π) β¦ π΄))βΆβ) |
90 | 70 | dmeqd 5862 |
. . . . . . . . . . . . 13
β’ (π β dom (β D (π₯ β (π(,)π) β¦ π΄)) = dom (π₯ β (π(,)π) β¦ π΅)) |
91 | 69 | ralrimiva 3140 |
. . . . . . . . . . . . . 14
β’ (π β βπ₯ β (π(,)π)π΅ β V) |
92 | | dmmptg 6195 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
(π(,)π)π΅ β V β dom (π₯ β (π(,)π) β¦ π΅) = (π(,)π)) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β dom (π₯ β (π(,)π) β¦ π΅) = (π(,)π)) |
94 | 90, 93 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β dom (β D (π₯ β (π(,)π) β¦ π΄)) = (π(,)π)) |
95 | 70, 94 | feq12d 6657 |
. . . . . . . . . . 11
β’ (π β ((β D (π₯ β (π(,)π) β¦ π΄)):dom (β D (π₯ β (π(,)π) β¦ π΄))βΆβ β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ)) |
96 | 89, 95 | mpbid 231 |
. . . . . . . . . 10
β’ (π β (π₯ β (π(,)π) β¦ π΅):(π(,)π)βΆβ) |
97 | 96 | fvmptelcdm 7062 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(,)π)) β π΅ β β) |
98 | 85, 97 | resubcld 11588 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(,)π)) β (π· β π΅) β β) |
99 | 85, 97 | subge0d 11750 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π(,)π)) β (0 β€ (π· β π΅) β π΅ β€ π·)) |
100 | 61, 99 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π₯ β (π(,)π)) β 0 β€ (π· β π΅)) |
101 | | elrege0 13377 |
. . . . . . . 8
β’ ((π· β π΅) β (0[,)+β) β ((π· β π΅) β β β§ 0 β€ (π· β π΅))) |
102 | 98, 100, 101 | sylanbrc 584 |
. . . . . . 7
β’ ((π β§ π₯ β (π(,)π)) β (π· β π΅) β (0[,)+β)) |
103 | 72, 102 | fmpt3d 7065 |
. . . . . 6
β’ (π β (β D (π₯ β (π[,]π) β¦ (πΆ β π΄))):(π(,)π)βΆ(0[,)+β)) |
104 | | dvle.l |
. . . . . 6
β’ (π β π β€ π) |
105 | 37, 38, 43, 103, 22, 9, 104 | dvge0 25386 |
. . . . 5
β’ (π β ((π₯ β (π[,]π) β¦ (πΆ β π΄))βπ) β€ ((π₯ β (π[,]π) β¦ (πΆ β π΄))βπ)) |
106 | 20, 25 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = π β (πΆ β π΄) = (π β π)) |
107 | | eqid 2733 |
. . . . . . 7
β’ (π₯ β (π[,]π) β¦ (πΆ β π΄)) = (π₯ β (π[,]π) β¦ (πΆ β π΄)) |
108 | | ovex 7391 |
. . . . . . 7
β’ (πΆ β π΄) β V |
109 | 106, 107,
108 | fvmpt3i 6954 |
. . . . . 6
β’ (π β (π[,]π) β ((π₯ β (π[,]π) β¦ (πΆ β π΄))βπ) = (π β π)) |
110 | 22, 109 | syl 17 |
. . . . 5
β’ (π β ((π₯ β (π[,]π) β¦ (πΆ β π΄))βπ) = (π β π)) |
111 | 11, 1 | oveq12d 7376 |
. . . . . . 7
β’ (π₯ = π β (πΆ β π΄) = (π β π
)) |
112 | 111, 107,
108 | fvmpt3i 6954 |
. . . . . 6
β’ (π β (π[,]π) β ((π₯ β (π[,]π) β¦ (πΆ β π΄))βπ) = (π β π
)) |
113 | 9, 112 | syl 17 |
. . . . 5
β’ (π β ((π₯ β (π[,]π) β¦ (πΆ β π΄))βπ) = (π β π
)) |
114 | 105, 110,
113 | 3brtr3d 5137 |
. . . 4
β’ (π β (π β π) β€ (π β π
)) |
115 | 23, 27, 36, 114 | subled 11763 |
. . 3
β’ (π β (π β (π β π
)) β€ π) |
116 | 35, 115 | eqbrtrd 5128 |
. 2
β’ (π β (π
β (π β π)) β€ π) |
117 | 10, 24, 27, 116 | subled 11763 |
1
β’ (π β (π
β π) β€ (π β π)) |