Step | Hyp | Ref
| Expression |
1 | | lebnum.c |
. . 3
β’ (π β π½ β Comp) |
2 | | lebnum.s |
. . 3
β’ (π β π β π½) |
3 | | lebnum.d |
. . . . . 6
β’ (π β π· β (Metβπ)) |
4 | | metxmet 23703 |
. . . . . 6
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β π· β (βMetβπ)) |
6 | | lebnum.j |
. . . . . 6
β’ π½ = (MetOpenβπ·) |
7 | 6 | mopnuni 23810 |
. . . . 5
β’ (π· β (βMetβπ) β π = βͺ π½) |
8 | 5, 7 | syl 17 |
. . . 4
β’ (π β π = βͺ π½) |
9 | | lebnum.u |
. . . 4
β’ (π β π = βͺ π) |
10 | 8, 9 | eqtr3d 2775 |
. . 3
β’ (π β βͺ π½ =
βͺ π) |
11 | | eqid 2733 |
. . . 4
β’ βͺ π½ =
βͺ π½ |
12 | 11 | cmpcov 22756 |
. . 3
β’ ((π½ β Comp β§ π β π½ β§ βͺ π½ = βͺ
π) β βπ€ β (π« π β© Fin)βͺ π½ =
βͺ π€) |
13 | 1, 2, 10, 12 | syl3anc 1372 |
. 2
β’ (π β βπ€ β (π« π β© Fin)βͺ
π½ = βͺ π€) |
14 | | 1rp 12924 |
. . . 4
β’ 1 β
β+ |
15 | | simprl 770 |
. . . . . . . . . 10
β’ ((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β π€ β (π« π β© Fin)) |
16 | 15 | elin1d 4159 |
. . . . . . . . 9
β’ ((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β π€ β π« π) |
17 | 16 | elpwid 4570 |
. . . . . . . 8
β’ ((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β π€ β π) |
18 | 17 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β§ π₯ β π) β π€ β π) |
19 | | simplr 768 |
. . . . . . 7
β’ ((((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β§ π₯ β π) β π β π€) |
20 | 18, 19 | sseldd 3946 |
. . . . . 6
β’ ((((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β§ π₯ β π) β π β π) |
21 | 5 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β§ π₯ β π) β π· β (βMetβπ)) |
22 | | simpr 486 |
. . . . . . 7
β’ ((((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β§ π₯ β π) β π₯ β π) |
23 | | rpxr 12929 |
. . . . . . . 8
β’ (1 β
β+ β 1 β β*) |
24 | 14, 23 | mp1i 13 |
. . . . . . 7
β’ ((((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β§ π₯ β π) β 1 β
β*) |
25 | | blssm 23787 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π₯ β π β§ 1 β β*) β
(π₯(ballβπ·)1) β π) |
26 | 21, 22, 24, 25 | syl3anc 1372 |
. . . . . 6
β’ ((((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β§ π₯ β π) β (π₯(ballβπ·)1) β π) |
27 | | sseq2 3971 |
. . . . . . 7
β’ (π’ = π β ((π₯(ballβπ·)1) β π’ β (π₯(ballβπ·)1) β π)) |
28 | 27 | rspcev 3580 |
. . . . . 6
β’ ((π β π β§ (π₯(ballβπ·)1) β π) β βπ’ β π (π₯(ballβπ·)1) β π’) |
29 | 20, 26, 28 | syl2anc 585 |
. . . . 5
β’ ((((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β§ π₯ β π) β βπ’ β π (π₯(ballβπ·)1) β π’) |
30 | 29 | ralrimiva 3140 |
. . . 4
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β βπ₯ β π βπ’ β π (π₯(ballβπ·)1) β π’) |
31 | | oveq2 7366 |
. . . . . . . 8
β’ (π = 1 β (π₯(ballβπ·)π) = (π₯(ballβπ·)1)) |
32 | 31 | sseq1d 3976 |
. . . . . . 7
β’ (π = 1 β ((π₯(ballβπ·)π) β π’ β (π₯(ballβπ·)1) β π’)) |
33 | 32 | rexbidv 3172 |
. . . . . 6
β’ (π = 1 β (βπ’ β π (π₯(ballβπ·)π) β π’ β βπ’ β π (π₯(ballβπ·)1) β π’)) |
34 | 33 | ralbidv 3171 |
. . . . 5
β’ (π = 1 β (βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’ β βπ₯ β π βπ’ β π (π₯(ballβπ·)1) β π’)) |
35 | 34 | rspcev 3580 |
. . . 4
β’ ((1
β β+ β§ βπ₯ β π βπ’ β π (π₯(ballβπ·)1) β π’) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
36 | 14, 30, 35 | sylancr 588 |
. . 3
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ π β π€) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
37 | 3 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β π· β (Metβπ)) |
38 | 1 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β π½ β Comp) |
39 | 17 | adantr 482 |
. . . . . 6
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β π€ β π) |
40 | 2 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β π β π½) |
41 | 39, 40 | sstrd 3955 |
. . . . 5
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β π€ β π½) |
42 | 8 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β π = βͺ π½) |
43 | | simplrr 777 |
. . . . . 6
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β βͺ π½ = βͺ
π€) |
44 | 42, 43 | eqtrd 2773 |
. . . . 5
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β π = βͺ π€) |
45 | 15 | elin2d 4160 |
. . . . . 6
β’ ((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β π€ β Fin) |
46 | 45 | adantr 482 |
. . . . 5
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β π€ β Fin) |
47 | | simpr 486 |
. . . . 5
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β Β¬ π β π€) |
48 | | eqid 2733 |
. . . . 5
β’ (π¦ β π β¦ Ξ£π β π€ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )) = (π¦ β π β¦ Ξ£π β π€ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
49 | | eqid 2733 |
. . . . 5
β’
(topGenβran (,)) = (topGenβran (,)) |
50 | 6, 37, 38, 41, 44, 46, 47, 48, 49 | lebnumlem3 24342 |
. . . 4
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β βπ β β+ βπ₯ β π βπ’ β π€ (π₯(ballβπ·)π) β π’) |
51 | | ssrexv 4012 |
. . . . . . 7
β’ (π€ β π β (βπ’ β π€ (π₯(ballβπ·)π) β π’ β βπ’ β π (π₯(ballβπ·)π) β π’)) |
52 | 39, 51 | syl 17 |
. . . . . 6
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β (βπ’ β π€ (π₯(ballβπ·)π) β π’ β βπ’ β π (π₯(ballβπ·)π) β π’)) |
53 | 52 | ralimdv 3163 |
. . . . 5
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β (βπ₯ β π βπ’ β π€ (π₯(ballβπ·)π) β π’ β βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’)) |
54 | 53 | reximdv 3164 |
. . . 4
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β (βπ β β+ βπ₯ β π βπ’ β π€ (π₯(ballβπ·)π) β π’ β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’)) |
55 | 50, 54 | mpd 15 |
. . 3
β’ (((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β§ Β¬ π β π€) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
56 | 36, 55 | pm2.61dan 812 |
. 2
β’ ((π β§ (π€ β (π« π β© Fin) β§ βͺ π½ =
βͺ π€)) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
57 | 13, 56 | rexlimddv 3155 |
1
β’ (π β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |