Step | Hyp | Ref
| Expression |
1 | | 0re 11164 |
. . . . . . 7
β’ 0 β
β |
2 | 1 | ne0ii 4302 |
. . . . . 6
β’ β
β β
|
3 | | 0ss 4361 |
. . . . . . . 8
β’ β
β (π(ballβπ)π) |
4 | | sseq1 3974 |
. . . . . . . 8
β’ (π = β
β (π β (π(ballβπ)π) β β
β (π(ballβπ)π))) |
5 | 3, 4 | mpbiri 258 |
. . . . . . 7
β’ (π = β
β π β (π(ballβπ)π)) |
6 | 5 | ralrimivw 3148 |
. . . . . 6
β’ (π = β
β βπ β β π β (π(ballβπ)π)) |
7 | | r19.2z 4457 |
. . . . . 6
β’ ((β
β β
β§ βπ β β π β (π(ballβπ)π)) β βπ β β π β (π(ballβπ)π)) |
8 | 2, 6, 7 | sylancr 588 |
. . . . 5
β’ (π = β
β βπ β β π β (π(ballβπ)π)) |
9 | 8 | a1i 11 |
. . . 4
β’ (((π β (Metβπ) β§ π β π) β§ π β (Bndβπ)) β (π = β
β βπ β β π β (π(ballβπ)π))) |
10 | | isbnd2 36271 |
. . . . . 6
β’ ((π β (Bndβπ) β§ π β β
) β (π β (βMetβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
11 | | simplll 774 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π β (Metβπ)) |
12 | | ssbnd.2 |
. . . . . . . . . . . . . . . . . . . . 21
β’ π = (π βΎ (π Γ π)) |
13 | 12 | dmeqi 5865 |
. . . . . . . . . . . . . . . . . . . 20
β’ dom π = dom (π βΎ (π Γ π)) |
14 | | dmres 5964 |
. . . . . . . . . . . . . . . . . . . 20
β’ dom
(π βΎ (π Γ π)) = ((π Γ π) β© dom π) |
15 | 13, 14 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . 19
β’ dom π = ((π Γ π) β© dom π) |
16 | | xmetf 23698 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (βMetβπ) β π:(π Γ π)βΆβ*) |
17 | 16 | fdmd 6684 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (βMetβπ) β dom π = (π Γ π)) |
18 | 15, 17 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (βMetβπ) β ((π Γ π) β© dom π) = (π Γ π)) |
19 | | df-ss 3932 |
. . . . . . . . . . . . . . . . . 18
β’ ((π Γ π) β dom π β ((π Γ π) β© dom π) = (π Γ π)) |
20 | 18, 19 | sylibr 233 |
. . . . . . . . . . . . . . . . 17
β’ (π β (βMetβπ) β (π Γ π) β dom π) |
21 | 20 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π Γ π) β dom π) |
22 | | metf 23699 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (Metβπ) β π:(π Γ π)βΆβ) |
23 | 22 | fdmd 6684 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Metβπ) β dom π = (π Γ π)) |
24 | 23 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β dom
π = (π Γ π)) |
25 | 21, 24 | sseqtrd 3989 |
. . . . . . . . . . . . . . 15
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π Γ π) β (π Γ π)) |
26 | | dmss 5863 |
. . . . . . . . . . . . . . 15
β’ ((π Γ π) β (π Γ π) β dom (π Γ π) β dom (π Γ π)) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β dom
(π Γ π) β dom (π Γ π)) |
28 | | dmxpid 5890 |
. . . . . . . . . . . . . 14
β’ dom
(π Γ π) = π |
29 | | dmxpid 5890 |
. . . . . . . . . . . . . 14
β’ dom
(π Γ π) = π |
30 | 27, 28, 29 | 3sstr3g 3993 |
. . . . . . . . . . . . 13
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π β π) |
31 | | simprl 770 |
. . . . . . . . . . . . 13
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π¦ β π) |
32 | 30, 31 | sseldd 3950 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π¦ β π) |
33 | | simpllr 775 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π β π) |
34 | | metcl 23701 |
. . . . . . . . . . . 12
β’ ((π β (Metβπ) β§ π¦ β π β§ π β π) β (π¦ππ) β β) |
35 | 11, 32, 33, 34 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π¦ππ) β β) |
36 | | rpre 12930 |
. . . . . . . . . . . 12
β’ (π β β+
β π β
β) |
37 | 36 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π β
β) |
38 | 35, 37 | readdcld 11191 |
. . . . . . . . . 10
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β ((π¦ππ) + π) β β) |
39 | | metxmet 23703 |
. . . . . . . . . . . . 13
β’ (π β (Metβπ) β π β (βMetβπ)) |
40 | 11, 39 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π β (βMetβπ)) |
41 | 32, 31 | elind 4159 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π¦ β (π β© π)) |
42 | | rpxr 12931 |
. . . . . . . . . . . . 13
β’ (π β β+
β π β
β*) |
43 | 42 | ad2antll 728 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π β
β*) |
44 | 12 | blres 23800 |
. . . . . . . . . . . 12
β’ ((π β (βMetβπ) β§ π¦ β (π β© π) β§ π β β*) β (π¦(ballβπ)π) = ((π¦(ballβπ)π) β© π)) |
45 | 40, 41, 43, 44 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π¦(ballβπ)π) = ((π¦(ballβπ)π) β© π)) |
46 | | inss1 4193 |
. . . . . . . . . . . 12
β’ ((π¦(ballβπ)π) β© π) β (π¦(ballβπ)π) |
47 | 35 | leidd 11728 |
. . . . . . . . . . . . . 14
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π¦ππ) β€ (π¦ππ)) |
48 | 35 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π¦ππ) β β) |
49 | 37 | recnd 11190 |
. . . . . . . . . . . . . . 15
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β π β
β) |
50 | 48, 49 | pncand 11520 |
. . . . . . . . . . . . . 14
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (((π¦ππ) + π) β π) = (π¦ππ)) |
51 | 47, 50 | breqtrrd 5138 |
. . . . . . . . . . . . 13
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π¦ππ) β€ (((π¦ππ) + π) β π)) |
52 | | blss2 23773 |
. . . . . . . . . . . . 13
β’ (((π β (βMetβπ) β§ π¦ β π β§ π β π) β§ (π β β β§ ((π¦ππ) + π) β β β§ (π¦ππ) β€ (((π¦ππ) + π) β π))) β (π¦(ballβπ)π) β (π(ballβπ)((π¦ππ) + π))) |
53 | 40, 32, 33, 37, 38, 51, 52 | syl33anc 1386 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π¦(ballβπ)π) β (π(ballβπ)((π¦ππ) + π))) |
54 | 46, 53 | sstrid 3960 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β ((π¦(ballβπ)π) β© π) β (π(ballβπ)((π¦ππ) + π))) |
55 | 45, 54 | eqsstrd 3987 |
. . . . . . . . . 10
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π¦(ballβπ)π) β (π(ballβπ)((π¦ππ) + π))) |
56 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π = ((π¦ππ) + π) β (π(ballβπ)π) = (π(ballβπ)((π¦ππ) + π))) |
57 | 56 | sseq2d 3981 |
. . . . . . . . . . 11
β’ (π = ((π¦ππ) + π) β ((π¦(ballβπ)π) β (π(ballβπ)π) β (π¦(ballβπ)π) β (π(ballβπ)((π¦ππ) + π)))) |
58 | 57 | rspcev 3584 |
. . . . . . . . . 10
β’ ((((π¦ππ) + π) β β β§ (π¦(ballβπ)π) β (π(ballβπ)((π¦ππ) + π))) β βπ β β (π¦(ballβπ)π) β (π(ballβπ)π)) |
59 | 38, 55, 58 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β
βπ β β
(π¦(ballβπ)π) β (π(ballβπ)π)) |
60 | | sseq1 3974 |
. . . . . . . . . 10
β’ (π = (π¦(ballβπ)π) β (π β (π(ballβπ)π) β (π¦(ballβπ)π) β (π(ballβπ)π))) |
61 | 60 | rexbidv 3176 |
. . . . . . . . 9
β’ (π = (π¦(ballβπ)π) β (βπ β β π β (π(ballβπ)π) β βπ β β (π¦(ballβπ)π) β (π(ballβπ)π))) |
62 | 59, 61 | syl5ibrcom 247 |
. . . . . . . 8
β’ ((((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β§ (π¦ β π β§ π β β+)) β (π = (π¦(ballβπ)π) β βπ β β π β (π(ballβπ)π))) |
63 | 62 | rexlimdvva 3206 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π β π) β§ π β (βMetβπ)) β (βπ¦ β π βπ β β+ π = (π¦(ballβπ)π) β βπ β β π β (π(ballβπ)π))) |
64 | 63 | expimpd 455 |
. . . . . 6
β’ ((π β (Metβπ) β§ π β π) β ((π β (βMetβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π)) β βπ β β π β (π(ballβπ)π))) |
65 | 10, 64 | biimtrid 241 |
. . . . 5
β’ ((π β (Metβπ) β§ π β π) β ((π β (Bndβπ) β§ π β β
) β βπ β β π β (π(ballβπ)π))) |
66 | 65 | expdimp 454 |
. . . 4
β’ (((π β (Metβπ) β§ π β π) β§ π β (Bndβπ)) β (π β β
β βπ β β π β (π(ballβπ)π))) |
67 | 9, 66 | pm2.61dne 3032 |
. . 3
β’ (((π β (Metβπ) β§ π β π) β§ π β (Bndβπ)) β βπ β β π β (π(ballβπ)π)) |
68 | 67 | ex 414 |
. 2
β’ ((π β (Metβπ) β§ π β π) β (π β (Bndβπ) β βπ β β π β (π(ballβπ)π))) |
69 | | simprr 772 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π β π) β§ (π β β β§ π β (π(ballβπ)π))) β π β (π(ballβπ)π)) |
70 | | xpss12 5653 |
. . . . . . 7
β’ ((π β (π(ballβπ)π) β§ π β (π(ballβπ)π)) β (π Γ π) β ((π(ballβπ)π) Γ (π(ballβπ)π))) |
71 | 69, 69, 70 | syl2anc 585 |
. . . . . 6
β’ (((π β (Metβπ) β§ π β π) β§ (π β β β§ π β (π(ballβπ)π))) β (π Γ π) β ((π(ballβπ)π) Γ (π(ballβπ)π))) |
72 | 71 | resabs1d 5973 |
. . . . 5
β’ (((π β (Metβπ) β§ π β π) β§ (π β β β§ π β (π(ballβπ)π))) β ((π βΎ ((π(ballβπ)π) Γ (π(ballβπ)π))) βΎ (π Γ π)) = (π βΎ (π Γ π))) |
73 | 72, 12 | eqtr4di 2795 |
. . . 4
β’ (((π β (Metβπ) β§ π β π) β§ (π β β β§ π β (π(ballβπ)π))) β ((π βΎ ((π(ballβπ)π) Γ (π(ballβπ)π))) βΎ (π Γ π)) = π) |
74 | | blbnd 36275 |
. . . . . . . 8
β’ ((π β (βMetβπ) β§ π β π β§ π β β) β (π βΎ ((π(ballβπ)π) Γ (π(ballβπ)π))) β (Bndβ(π(ballβπ)π))) |
75 | 39, 74 | syl3an1 1164 |
. . . . . . 7
β’ ((π β (Metβπ) β§ π β π β§ π β β) β (π βΎ ((π(ballβπ)π) Γ (π(ballβπ)π))) β (Bndβ(π(ballβπ)π))) |
76 | 75 | 3expa 1119 |
. . . . . 6
β’ (((π β (Metβπ) β§ π β π) β§ π β β) β (π βΎ ((π(ballβπ)π) Γ (π(ballβπ)π))) β (Bndβ(π(ballβπ)π))) |
77 | 76 | adantrr 716 |
. . . . 5
β’ (((π β (Metβπ) β§ π β π) β§ (π β β β§ π β (π(ballβπ)π))) β (π βΎ ((π(ballβπ)π) Γ (π(ballβπ)π))) β (Bndβ(π(ballβπ)π))) |
78 | | bndss 36274 |
. . . . 5
β’ (((π βΎ ((π(ballβπ)π) Γ (π(ballβπ)π))) β (Bndβ(π(ballβπ)π)) β§ π β (π(ballβπ)π)) β ((π βΎ ((π(ballβπ)π) Γ (π(ballβπ)π))) βΎ (π Γ π)) β (Bndβπ)) |
79 | 77, 69, 78 | syl2anc 585 |
. . . 4
β’ (((π β (Metβπ) β§ π β π) β§ (π β β β§ π β (π(ballβπ)π))) β ((π βΎ ((π(ballβπ)π) Γ (π(ballβπ)π))) βΎ (π Γ π)) β (Bndβπ)) |
80 | 73, 79 | eqeltrrd 2839 |
. . 3
β’ (((π β (Metβπ) β§ π β π) β§ (π β β β§ π β (π(ballβπ)π))) β π β (Bndβπ)) |
81 | 80 | rexlimdvaa 3154 |
. 2
β’ ((π β (Metβπ) β§ π β π) β (βπ β β π β (π(ballβπ)π) β π β (Bndβπ))) |
82 | 68, 81 | impbid 211 |
1
β’ ((π β (Metβπ) β§ π β π) β (π β (Bndβπ) β βπ β β π β (π(ballβπ)π))) |