Step | Hyp | Ref
| Expression |
1 | | bndth.1 |
. . 3
β’ π = βͺ
π½ |
2 | | bndth.2 |
. . 3
β’ πΎ = (topGenβran
(,)) |
3 | | bndth.3 |
. . 3
β’ (π β π½ β Comp) |
4 | | cmptop 22899 |
. . . . . 6
β’ (π½ β Comp β π½ β Top) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β π½ β Top) |
6 | 1 | toptopon 22419 |
. . . . 5
β’ (π½ β Top β π½ β (TopOnβπ)) |
7 | 5, 6 | sylib 217 |
. . . 4
β’ (π β π½ β (TopOnβπ)) |
8 | | bndth.4 |
. . . . . . 7
β’ (π β πΉ β (π½ Cn πΎ)) |
9 | | uniretop 24279 |
. . . . . . . . 9
β’ β =
βͺ (topGenβran (,)) |
10 | 2 | unieqi 4922 |
. . . . . . . . 9
β’ βͺ πΎ =
βͺ (topGenβran (,)) |
11 | 9, 10 | eqtr4i 2764 |
. . . . . . . 8
β’ β =
βͺ πΎ |
12 | 1, 11 | cnf 22750 |
. . . . . . 7
β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆβ) |
13 | 8, 12 | syl 17 |
. . . . . 6
β’ (π β πΉ:πβΆβ) |
14 | 13 | feqmptd 6961 |
. . . . 5
β’ (π β πΉ = (π§ β π β¦ (πΉβπ§))) |
15 | 14, 8 | eqeltrrd 2835 |
. . . 4
β’ (π β (π§ β π β¦ (πΉβπ§)) β (π½ Cn πΎ)) |
16 | | retopon 24280 |
. . . . . 6
β’
(topGenβran (,)) β (TopOnββ) |
17 | 2, 16 | eqeltri 2830 |
. . . . 5
β’ πΎ β
(TopOnββ) |
18 | 17 | a1i 11 |
. . . 4
β’ (π β πΎ β
(TopOnββ)) |
19 | | eqid 2733 |
. . . . . . . . . 10
β’
(TopOpenββfld) =
(TopOpenββfld) |
20 | 19 | cnfldtopon 24299 |
. . . . . . . . 9
β’
(TopOpenββfld) β
(TopOnββ) |
21 | 20 | a1i 11 |
. . . . . . . 8
β’ (π β
(TopOpenββfld) β
(TopOnββ)) |
22 | | 0cnd 11207 |
. . . . . . . 8
β’ (π β 0 β
β) |
23 | 18, 21, 22 | cnmptc 23166 |
. . . . . . 7
β’ (π β (π¦ β β β¦ 0) β (πΎ Cn
(TopOpenββfld))) |
24 | 19 | tgioo2 24319 |
. . . . . . . . 9
β’
(topGenβran (,)) = ((TopOpenββfld)
βΎt β) |
25 | 2, 24 | eqtri 2761 |
. . . . . . . 8
β’ πΎ =
((TopOpenββfld) βΎt
β) |
26 | | ax-resscn 11167 |
. . . . . . . . 9
β’ β
β β |
27 | 26 | a1i 11 |
. . . . . . . 8
β’ (π β β β
β) |
28 | 21 | cnmptid 23165 |
. . . . . . . 8
β’ (π β (π¦ β β β¦ π¦) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
29 | 25, 21, 27, 28 | cnmpt1res 23180 |
. . . . . . 7
β’ (π β (π¦ β β β¦ π¦) β (πΎ Cn
(TopOpenββfld))) |
30 | 19 | subcn 24382 |
. . . . . . . 8
β’ β
β (((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld)) |
31 | 30 | a1i 11 |
. . . . . . 7
β’ (π β β β
(((TopOpenββfld) Γt
(TopOpenββfld)) Cn
(TopOpenββfld))) |
32 | 18, 23, 29, 31 | cnmpt12f 23170 |
. . . . . 6
β’ (π β (π¦ β β β¦ (0 β π¦)) β (πΎ Cn
(TopOpenββfld))) |
33 | | df-neg 11447 |
. . . . . . . . . . 11
β’ -π¦ = (0 β π¦) |
34 | | renegcl 11523 |
. . . . . . . . . . 11
β’ (π¦ β β β -π¦ β
β) |
35 | 33, 34 | eqeltrrid 2839 |
. . . . . . . . . 10
β’ (π¦ β β β (0
β π¦) β
β) |
36 | 35 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π¦ β β) β (0 β π¦) β
β) |
37 | 36 | fmpttd 7115 |
. . . . . . . 8
β’ (π β (π¦ β β β¦ (0 β π¦)):ββΆβ) |
38 | 37 | frnd 6726 |
. . . . . . 7
β’ (π β ran (π¦ β β β¦ (0 β π¦)) β
β) |
39 | | cnrest2 22790 |
. . . . . . 7
β’
(((TopOpenββfld) β (TopOnββ)
β§ ran (π¦ β β
β¦ (0 β π¦))
β β β§ β β β) β ((π¦ β β β¦ (0 β π¦)) β (πΎ Cn (TopOpenββfld))
β (π¦ β β
β¦ (0 β π¦))
β (πΎ Cn
((TopOpenββfld) βΎt
β)))) |
40 | 21, 38, 27, 39 | syl3anc 1372 |
. . . . . 6
β’ (π β ((π¦ β β β¦ (0 β π¦)) β (πΎ Cn (TopOpenββfld))
β (π¦ β β
β¦ (0 β π¦))
β (πΎ Cn
((TopOpenββfld) βΎt
β)))) |
41 | 32, 40 | mpbid 231 |
. . . . 5
β’ (π β (π¦ β β β¦ (0 β π¦)) β (πΎ Cn ((TopOpenββfld)
βΎt β))) |
42 | 25 | oveq2i 7420 |
. . . . 5
β’ (πΎ Cn πΎ) = (πΎ Cn ((TopOpenββfld)
βΎt β)) |
43 | 41, 42 | eleqtrrdi 2845 |
. . . 4
β’ (π β (π¦ β β β¦ (0 β π¦)) β (πΎ Cn πΎ)) |
44 | | negeq 11452 |
. . . . 5
β’ (π¦ = (πΉβπ§) β -π¦ = -(πΉβπ§)) |
45 | 33, 44 | eqtr3id 2787 |
. . . 4
β’ (π¦ = (πΉβπ§) β (0 β π¦) = -(πΉβπ§)) |
46 | 7, 15, 18, 43, 45 | cnmpt11 23167 |
. . 3
β’ (π β (π§ β π β¦ -(πΉβπ§)) β (π½ Cn πΎ)) |
47 | | evth.5 |
. . 3
β’ (π β π β β
) |
48 | 1, 2, 3, 46, 47 | evth 24475 |
. 2
β’ (π β βπ₯ β π βπ¦ β π ((π§ β π β¦ -(πΉβπ§))βπ¦) β€ ((π§ β π β¦ -(πΉβπ§))βπ₯)) |
49 | | fveq2 6892 |
. . . . . . . . 9
β’ (π§ = π¦ β (πΉβπ§) = (πΉβπ¦)) |
50 | 49 | negeqd 11454 |
. . . . . . . 8
β’ (π§ = π¦ β -(πΉβπ§) = -(πΉβπ¦)) |
51 | | eqid 2733 |
. . . . . . . 8
β’ (π§ β π β¦ -(πΉβπ§)) = (π§ β π β¦ -(πΉβπ§)) |
52 | | negex 11458 |
. . . . . . . 8
β’ -(πΉβπ¦) β V |
53 | 50, 51, 52 | fvmpt 6999 |
. . . . . . 7
β’ (π¦ β π β ((π§ β π β¦ -(πΉβπ§))βπ¦) = -(πΉβπ¦)) |
54 | 53 | adantl 483 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π¦ β π) β ((π§ β π β¦ -(πΉβπ§))βπ¦) = -(πΉβπ¦)) |
55 | | fveq2 6892 |
. . . . . . . . 9
β’ (π§ = π₯ β (πΉβπ§) = (πΉβπ₯)) |
56 | 55 | negeqd 11454 |
. . . . . . . 8
β’ (π§ = π₯ β -(πΉβπ§) = -(πΉβπ₯)) |
57 | | negex 11458 |
. . . . . . . 8
β’ -(πΉβπ₯) β V |
58 | 56, 51, 57 | fvmpt 6999 |
. . . . . . 7
β’ (π₯ β π β ((π§ β π β¦ -(πΉβπ§))βπ₯) = -(πΉβπ₯)) |
59 | 58 | ad2antlr 726 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π¦ β π) β ((π§ β π β¦ -(πΉβπ§))βπ₯) = -(πΉβπ₯)) |
60 | 54, 59 | breq12d 5162 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β (((π§ β π β¦ -(πΉβπ§))βπ¦) β€ ((π§ β π β¦ -(πΉβπ§))βπ₯) β -(πΉβπ¦) β€ -(πΉβπ₯))) |
61 | 13 | ffvelcdmda 7087 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (πΉβπ₯) β β) |
62 | 61 | adantr 482 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π¦ β π) β (πΉβπ₯) β β) |
63 | 13 | ffvelcdmda 7087 |
. . . . . . 7
β’ ((π β§ π¦ β π) β (πΉβπ¦) β β) |
64 | 63 | adantlr 714 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π¦ β π) β (πΉβπ¦) β β) |
65 | 62, 64 | lenegd 11793 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β ((πΉβπ₯) β€ (πΉβπ¦) β -(πΉβπ¦) β€ -(πΉβπ₯))) |
66 | 60, 65 | bitr4d 282 |
. . . 4
β’ (((π β§ π₯ β π) β§ π¦ β π) β (((π§ β π β¦ -(πΉβπ§))βπ¦) β€ ((π§ β π β¦ -(πΉβπ§))βπ₯) β (πΉβπ₯) β€ (πΉβπ¦))) |
67 | 66 | ralbidva 3176 |
. . 3
β’ ((π β§ π₯ β π) β (βπ¦ β π ((π§ β π β¦ -(πΉβπ§))βπ¦) β€ ((π§ β π β¦ -(πΉβπ§))βπ₯) β βπ¦ β π (πΉβπ₯) β€ (πΉβπ¦))) |
68 | 67 | rexbidva 3177 |
. 2
β’ (π β (βπ₯ β π βπ¦ β π ((π§ β π β¦ -(πΉβπ§))βπ¦) β€ ((π§ β π β¦ -(πΉβπ§))βπ₯) β βπ₯ β π βπ¦ β π (πΉβπ₯) β€ (πΉβπ¦))) |
69 | 48, 68 | mpbid 231 |
1
β’ (π β βπ₯ β π βπ¦ β π (πΉβπ₯) β€ (πΉβπ¦)) |