Step | Hyp | Ref
| Expression |
1 | | heibor.7 |
. . . . . . . 8
β’ (π β πΉ:β0βΆ(π« π β© Fin)) |
2 | | 0nn0 12386 |
. . . . . . . 8
β’ 0 β
β0 |
3 | | inss2 4187 |
. . . . . . . . 9
β’
(π« π β©
Fin) β Fin |
4 | | ffvelcdm 7029 |
. . . . . . . . 9
β’ ((πΉ:β0βΆ(π« π β© Fin) β§ 0 β
β0) β (πΉβ0) β (π« π β© Fin)) |
5 | 3, 4 | sselid 3940 |
. . . . . . . 8
β’ ((πΉ:β0βΆ(π« π β© Fin) β§ 0 β
β0) β (πΉβ0) β Fin) |
6 | 1, 2, 5 | sylancl 586 |
. . . . . . 7
β’ (π β (πΉβ0) β Fin) |
7 | | heibor.8 |
. . . . . . . . 9
β’ (π β βπ β β0 π = βͺ π¦ β (πΉβπ)(π¦π΅π)) |
8 | | fveq2 6839 |
. . . . . . . . . . . 12
β’ (π = 0 β (πΉβπ) = (πΉβ0)) |
9 | | oveq2 7359 |
. . . . . . . . . . . 12
β’ (π = 0 β (π¦π΅π) = (π¦π΅0)) |
10 | 8, 9 | iuneq12d 4980 |
. . . . . . . . . . 11
β’ (π = 0 β βͺ π¦ β (πΉβπ)(π¦π΅π) = βͺ π¦ β (πΉβ0)(π¦π΅0)) |
11 | 10 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (π = 0 β (π = βͺ π¦ β (πΉβπ)(π¦π΅π) β π = βͺ π¦ β (πΉβ0)(π¦π΅0))) |
12 | 11 | rspccva 3578 |
. . . . . . . . 9
β’
((βπ β
β0 π =
βͺ π¦ β (πΉβπ)(π¦π΅π) β§ 0 β β0) β
π = βͺ π¦ β (πΉβ0)(π¦π΅0)) |
13 | 7, 2, 12 | sylancl 586 |
. . . . . . . 8
β’ (π β π = βͺ π¦ β (πΉβ0)(π¦π΅0)) |
14 | | eqimss 3998 |
. . . . . . . 8
β’ (π = βͺ π¦ β (πΉβ0)(π¦π΅0) β π β βͺ
π¦ β (πΉβ0)(π¦π΅0)) |
15 | 13, 14 | syl 17 |
. . . . . . 7
β’ (π β π β βͺ
π¦ β (πΉβ0)(π¦π΅0)) |
16 | | heibor.1 |
. . . . . . . . . 10
β’ π½ = (MetOpenβπ·) |
17 | | heibor.3 |
. . . . . . . . . 10
β’ πΎ = {π’ β£ Β¬ βπ£ β (π« π β© Fin)π’ β βͺ π£} |
18 | | ovex 7384 |
. . . . . . . . . 10
β’ (π¦π΅0) β V |
19 | 16, 17, 18 | heiborlem1 36208 |
. . . . . . . . 9
β’ (((πΉβ0) β Fin β§ π β βͺ π¦ β (πΉβ0)(π¦π΅0) β§ π β πΎ) β βπ¦ β (πΉβ0)(π¦π΅0) β πΎ) |
20 | | oveq1 7358 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (π¦π΅0) = (π₯π΅0)) |
21 | 20 | eleq1d 2822 |
. . . . . . . . . 10
β’ (π¦ = π₯ β ((π¦π΅0) β πΎ β (π₯π΅0) β πΎ)) |
22 | 21 | cbvrexvw 3224 |
. . . . . . . . 9
β’
(βπ¦ β
(πΉβ0)(π¦π΅0) β πΎ β βπ₯ β (πΉβ0)(π₯π΅0) β πΎ) |
23 | 19, 22 | sylib 217 |
. . . . . . . 8
β’ (((πΉβ0) β Fin β§ π β βͺ π¦ β (πΉβ0)(π¦π΅0) β§ π β πΎ) β βπ₯ β (πΉβ0)(π₯π΅0) β πΎ) |
24 | 23 | 3expia 1121 |
. . . . . . 7
β’ (((πΉβ0) β Fin β§ π β βͺ π¦ β (πΉβ0)(π¦π΅0)) β (π β πΎ β βπ₯ β (πΉβ0)(π₯π΅0) β πΎ)) |
25 | 6, 15, 24 | syl2anc 584 |
. . . . . 6
β’ (π β (π β πΎ β βπ₯ β (πΉβ0)(π₯π΅0) β πΎ)) |
26 | 25 | adantr 481 |
. . . . 5
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β (π β πΎ β βπ₯ β (πΉβ0)(π₯π΅0) β πΎ)) |
27 | | heibor.4 |
. . . . . . . . . 10
β’ πΊ = {β¨π¦, πβ© β£ (π β β0 β§ π¦ β (πΉβπ) β§ (π¦π΅π) β πΎ)} |
28 | | vex 3447 |
. . . . . . . . . 10
β’ π₯ β V |
29 | | c0ex 11107 |
. . . . . . . . . 10
β’ 0 β
V |
30 | 16, 17, 27, 28, 29 | heiborlem2 36209 |
. . . . . . . . 9
β’ (π₯πΊ0 β (0 β β0 β§
π₯ β (πΉβ0) β§ (π₯π΅0) β πΎ)) |
31 | | heibor.5 |
. . . . . . . . . . . 12
β’ π΅ = (π§ β π, π β β0 β¦ (π§(ballβπ·)(1 / (2βπ)))) |
32 | | heibor.6 |
. . . . . . . . . . . 12
β’ (π β π· β (CMetβπ)) |
33 | 16, 17, 27, 31, 32, 1, 7 | heiborlem3 36210 |
. . . . . . . . . . 11
β’ (π β βπβπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ)) |
34 | 33 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π₯πΊ0) β βπβπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ)) |
35 | 32 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (π₯πΊ0 β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) β π· β (CMetβπ)) |
36 | 1 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (π₯πΊ0 β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) β πΉ:β0βΆ(π« π β© Fin)) |
37 | 7 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (π₯πΊ0 β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) β βπ β β0 π = βͺ π¦ β (πΉβπ)(π¦π΅π)) |
38 | | simprr 771 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (π₯πΊ0 β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) β βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ)) |
39 | | fveq2 6839 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π‘ β (πβπ₯) = (πβπ‘)) |
40 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π‘ β (2nd βπ₯) = (2nd βπ‘)) |
41 | 40 | oveq1d 7366 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π‘ β ((2nd βπ₯) + 1) = ((2nd
βπ‘) +
1)) |
42 | 39, 41 | breq12d 5116 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π‘ β ((πβπ₯)πΊ((2nd βπ₯) + 1) β (πβπ‘)πΊ((2nd βπ‘) + 1))) |
43 | | fveq2 6839 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π‘ β (π΅βπ₯) = (π΅βπ‘)) |
44 | 39, 41 | oveq12d 7369 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π‘ β ((πβπ₯)π΅((2nd βπ₯) + 1)) = ((πβπ‘)π΅((2nd βπ‘) + 1))) |
45 | 43, 44 | ineq12d 4171 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π‘ β ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) = ((π΅βπ‘) β© ((πβπ‘)π΅((2nd βπ‘) + 1)))) |
46 | 45 | eleq1d 2822 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π‘ β (((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ β ((π΅βπ‘) β© ((πβπ‘)π΅((2nd βπ‘) + 1))) β πΎ)) |
47 | 42, 46 | anbi12d 631 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π‘ β (((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ) β ((πβπ‘)πΊ((2nd βπ‘) + 1) β§ ((π΅βπ‘) β© ((πβπ‘)π΅((2nd βπ‘) + 1))) β πΎ))) |
48 | 47 | cbvralvw 3223 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ) β βπ‘ β πΊ ((πβπ‘)πΊ((2nd βπ‘) + 1) β§ ((π΅βπ‘) β© ((πβπ‘)π΅((2nd βπ‘) + 1))) β πΎ)) |
49 | 38, 48 | sylib 217 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (π₯πΊ0 β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) β βπ‘ β πΊ ((πβπ‘)πΊ((2nd βπ‘) + 1) β§ ((π΅βπ‘) β© ((πβπ‘)π΅((2nd βπ‘) + 1))) β πΎ)) |
50 | | simprl 769 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (π₯πΊ0 β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) β π₯πΊ0) |
51 | | eqeq1 2741 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π = 0 β π = 0)) |
52 | | oveq1 7358 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π β 1) = (π β 1)) |
53 | 51, 52 | ifbieq2d 4510 |
. . . . . . . . . . . . . . 15
β’ (π = π β if(π = 0, π₯, (π β 1)) = if(π = 0, π₯, (π β 1))) |
54 | 53 | cbvmptv 5216 |
. . . . . . . . . . . . . 14
β’ (π β β0
β¦ if(π = 0, π₯, (π β 1))) = (π β β0 β¦ if(π = 0, π₯, (π β 1))) |
55 | | seqeq3 13865 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β¦ if(π = 0, π₯, (π β 1))) = (π β β0 β¦ if(π = 0, π₯, (π β 1))) β seq0(π, (π β β0 β¦ if(π = 0, π₯, (π β 1)))) = seq0(π, (π β β0 β¦ if(π = 0, π₯, (π β 1))))) |
56 | 54, 55 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
seq0(π, (π β β0
β¦ if(π = 0, π₯, (π β 1)))) = seq0(π, (π β β0 β¦ if(π = 0, π₯, (π β 1)))) |
57 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π β β β¦
β¨(seq0(π, (π β β0
β¦ if(π = 0, π₯, (π β 1))))βπ), (3 / (2βπ))β©) = (π β β β¦ β¨(seq0(π, (π β β0 β¦ if(π = 0, π₯, (π β 1))))βπ), (3 / (2βπ))β©) |
58 | | simplrl 775 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (π₯πΊ0 β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) β π β π½) |
59 | | cmetmet 24602 |
. . . . . . . . . . . . . . . . 17
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
60 | | metxmet 23639 |
. . . . . . . . . . . . . . . . 17
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
61 | 16 | mopnuni 23746 |
. . . . . . . . . . . . . . . . 17
β’ (π· β (βMetβπ) β π = βͺ π½) |
62 | 32, 59, 60, 61 | 4syl 19 |
. . . . . . . . . . . . . . . 16
β’ (π β π = βͺ π½) |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β π = βͺ
π½) |
64 | | simprr 771 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β βͺ π½ =
βͺ π) |
65 | 63, 64 | eqtr2d 2778 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β βͺ π =
π) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (π₯πΊ0 β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) β βͺ
π = π) |
67 | 16, 17, 27, 31, 35, 36, 37, 49, 50, 56, 57, 58, 66 | heiborlem9 36216 |
. . . . . . . . . . . 12
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (π₯πΊ0 β§ βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ))) β Β¬ π β πΎ) |
68 | 67 | expr 457 |
. . . . . . . . . . 11
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π₯πΊ0) β (βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ) β Β¬ π β πΎ)) |
69 | 68 | exlimdv 1936 |
. . . . . . . . . 10
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π₯πΊ0) β (βπβπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ) β Β¬ π β πΎ)) |
70 | 34, 69 | mpd 15 |
. . . . . . . . 9
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π₯πΊ0) β Β¬ π β πΎ) |
71 | 30, 70 | sylan2br 595 |
. . . . . . . 8
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ (0 β
β0 β§ π₯
β (πΉβ0) β§
(π₯π΅0) β πΎ)) β Β¬ π β πΎ) |
72 | 71 | 3exp2 1354 |
. . . . . . 7
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β (0 β
β0 β (π₯ β (πΉβ0) β ((π₯π΅0) β πΎ β Β¬ π β πΎ)))) |
73 | 2, 72 | mpi 20 |
. . . . . 6
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β (π₯ β (πΉβ0) β ((π₯π΅0) β πΎ β Β¬ π β πΎ))) |
74 | 73 | rexlimdv 3148 |
. . . . 5
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β (βπ₯ β (πΉβ0)(π₯π΅0) β πΎ β Β¬ π β πΎ)) |
75 | 26, 74 | syld 47 |
. . . 4
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β (π β πΎ β Β¬ π β πΎ)) |
76 | 75 | pm2.01d 189 |
. . 3
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β Β¬ π β πΎ) |
77 | | elfvdm 6876 |
. . . . . 6
β’ (π· β (CMetβπ) β π β dom CMet) |
78 | | sseq1 3967 |
. . . . . . . . 9
β’ (π’ = π β (π’ β βͺ π£ β π β βͺ π£)) |
79 | 78 | rexbidv 3173 |
. . . . . . . 8
β’ (π’ = π β (βπ£ β (π« π β© Fin)π’ β βͺ π£ β βπ£ β (π« π β© Fin)π β βͺ π£)) |
80 | 79 | notbid 317 |
. . . . . . 7
β’ (π’ = π β (Β¬ βπ£ β (π« π β© Fin)π’ β βͺ π£ β Β¬ βπ£ β (π« π β© Fin)π β βͺ π£)) |
81 | 80, 17 | elab2g 3630 |
. . . . . 6
β’ (π β dom CMet β (π β πΎ β Β¬ βπ£ β (π« π β© Fin)π β βͺ π£)) |
82 | 32, 77, 81 | 3syl 18 |
. . . . 5
β’ (π β (π β πΎ β Β¬ βπ£ β (π« π β© Fin)π β βͺ π£)) |
83 | 82 | adantr 481 |
. . . 4
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β (π β πΎ β Β¬ βπ£ β (π« π β© Fin)π β βͺ π£)) |
84 | 83 | con2bid 354 |
. . 3
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β (βπ£ β (π« π β© Fin)π β βͺ π£ β Β¬ π β πΎ)) |
85 | 76, 84 | mpbird 256 |
. 2
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β βπ£ β (π« π β© Fin)π β βͺ π£) |
86 | 62 | ad2antrr 724 |
. . . . 5
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π£ β (π« π β© Fin)) β π = βͺ
π½) |
87 | 86 | sseq1d 3973 |
. . . 4
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π£ β (π« π β© Fin)) β (π β βͺ π£
β βͺ π½ β βͺ π£)) |
88 | | inss1 4186 |
. . . . . . . . 9
β’
(π« π β©
Fin) β π« π |
89 | 88 | sseli 3938 |
. . . . . . . 8
β’ (π£ β (π« π β© Fin) β π£ β π« π) |
90 | 89 | elpwid 4567 |
. . . . . . 7
β’ (π£ β (π« π β© Fin) β π£ β π) |
91 | | simprl 769 |
. . . . . . 7
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β π β π½) |
92 | | sstr 3950 |
. . . . . . . 8
β’ ((π£ β π β§ π β π½) β π£ β π½) |
93 | 92 | unissd 4873 |
. . . . . . 7
β’ ((π£ β π β§ π β π½) β βͺ π£ β βͺ π½) |
94 | 90, 91, 93 | syl2anr 597 |
. . . . . 6
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π£ β (π« π β© Fin)) β βͺ π£
β βͺ π½) |
95 | 94 | biantrud 532 |
. . . . 5
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π£ β (π« π β© Fin)) β (βͺ π½
β βͺ π£ β (βͺ π½ β βͺ π£
β§ βͺ π£ β βͺ π½))) |
96 | | eqss 3957 |
. . . . 5
β’ (βͺ π½ =
βͺ π£ β (βͺ π½ β βͺ π£
β§ βͺ π£ β βͺ π½)) |
97 | 95, 96 | bitr4di 288 |
. . . 4
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π£ β (π« π β© Fin)) β (βͺ π½
β βͺ π£ β βͺ π½ = βͺ
π£)) |
98 | 87, 97 | bitrd 278 |
. . 3
β’ (((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β§ π£ β (π« π β© Fin)) β (π β βͺ π£
β βͺ π½ = βͺ π£)) |
99 | 98 | rexbidva 3171 |
. 2
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β (βπ£ β (π« π β© Fin)π β βͺ π£ β βπ£ β (π« π β© Fin)βͺ π½ =
βͺ π£)) |
100 | 85, 99 | mpbid 231 |
1
β’ ((π β§ (π β π½ β§ βͺ π½ = βͺ
π)) β βπ£ β (π« π β© Fin)βͺ π½ =
βͺ π£) |