Step | Hyp | Ref
| Expression |
1 | | rfcnpre3.3 |
. . . . . . . 8
β’ πΎ = (topGenβran
(,)) |
2 | | rfcnpre3.4 |
. . . . . . . 8
β’ π = βͺ
π½ |
3 | | eqid 2733 |
. . . . . . . 8
β’ (π½ Cn πΎ) = (π½ Cn πΎ) |
4 | | rfcnpre3.8 |
. . . . . . . 8
β’ (π β πΉ β (π½ Cn πΎ)) |
5 | 1, 2, 3, 4 | fcnre 43318 |
. . . . . . 7
β’ (π β πΉ:πβΆβ) |
6 | | ffn 6669 |
. . . . . . 7
β’ (πΉ:πβΆβ β πΉ Fn π) |
7 | | elpreima 7009 |
. . . . . . 7
β’ (πΉ Fn π β (π β (β‘πΉ β (π΅[,)+β)) β (π β π β§ (πΉβπ ) β (π΅[,)+β)))) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . 6
β’ (π β (π β (β‘πΉ β (π΅[,)+β)) β (π β π β§ (πΉβπ ) β (π΅[,)+β)))) |
9 | | rfcnpre3.6 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
10 | 9 | rexrd 11210 |
. . . . . . . . . 10
β’ (π β π΅ β
β*) |
11 | 10 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π) β π΅ β
β*) |
12 | | pnfxr 11214 |
. . . . . . . . 9
β’ +β
β β* |
13 | | elico1 13313 |
. . . . . . . . 9
β’ ((π΅ β β*
β§ +β β β*) β ((πΉβπ ) β (π΅[,)+β) β ((πΉβπ ) β β* β§ π΅ β€ (πΉβπ ) β§ (πΉβπ ) < +β))) |
14 | 11, 12, 13 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π β π) β ((πΉβπ ) β (π΅[,)+β) β ((πΉβπ ) β β* β§ π΅ β€ (πΉβπ ) β§ (πΉβπ ) < +β))) |
15 | | simpr2 1196 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ ((πΉβπ ) β β* β§ π΅ β€ (πΉβπ ) β§ (πΉβπ ) < +β)) β π΅ β€ (πΉβπ )) |
16 | 5 | ffvelcdmda 7036 |
. . . . . . . . . . . 12
β’ ((π β§ π β π) β (πΉβπ ) β β) |
17 | 16 | rexrd 11210 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β (πΉβπ ) β
β*) |
18 | 17 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π΅ β€ (πΉβπ )) β (πΉβπ ) β
β*) |
19 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π΅ β€ (πΉβπ )) β π΅ β€ (πΉβπ )) |
20 | 16 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π) β§ π΅ β€ (πΉβπ )) β (πΉβπ ) β β) |
21 | | ltpnf 13046 |
. . . . . . . . . . 11
β’ ((πΉβπ ) β β β (πΉβπ ) < +β) |
22 | 20, 21 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β π) β§ π΅ β€ (πΉβπ )) β (πΉβπ ) < +β) |
23 | 18, 19, 22 | 3jca 1129 |
. . . . . . . . 9
β’ (((π β§ π β π) β§ π΅ β€ (πΉβπ )) β ((πΉβπ ) β β* β§ π΅ β€ (πΉβπ ) β§ (πΉβπ ) < +β)) |
24 | 15, 23 | impbida 800 |
. . . . . . . 8
β’ ((π β§ π β π) β (((πΉβπ ) β β* β§ π΅ β€ (πΉβπ ) β§ (πΉβπ ) < +β) β π΅ β€ (πΉβπ ))) |
25 | 14, 24 | bitrd 279 |
. . . . . . 7
β’ ((π β§ π β π) β ((πΉβπ ) β (π΅[,)+β) β π΅ β€ (πΉβπ ))) |
26 | 25 | pm5.32da 580 |
. . . . . 6
β’ (π β ((π β π β§ (πΉβπ ) β (π΅[,)+β)) β (π β π β§ π΅ β€ (πΉβπ )))) |
27 | 8, 26 | bitrd 279 |
. . . . 5
β’ (π β (π β (β‘πΉ β (π΅[,)+β)) β (π β π β§ π΅ β€ (πΉβπ )))) |
28 | | nfcv 2904 |
. . . . . 6
β’
β²π‘π |
29 | | nfcv 2904 |
. . . . . 6
β’
β²π‘π |
30 | | nfcv 2904 |
. . . . . . 7
β’
β²π‘π΅ |
31 | | nfcv 2904 |
. . . . . . 7
β’
β²π‘
β€ |
32 | | rfcnpre3.2 |
. . . . . . . 8
β’
β²π‘πΉ |
33 | 32, 28 | nffv 6853 |
. . . . . . 7
β’
β²π‘(πΉβπ ) |
34 | 30, 31, 33 | nfbr 5153 |
. . . . . 6
β’
β²π‘ π΅ β€ (πΉβπ ) |
35 | | fveq2 6843 |
. . . . . . 7
β’ (π‘ = π β (πΉβπ‘) = (πΉβπ )) |
36 | 35 | breq2d 5118 |
. . . . . 6
β’ (π‘ = π β (π΅ β€ (πΉβπ‘) β π΅ β€ (πΉβπ ))) |
37 | 28, 29, 34, 36 | elrabf 3642 |
. . . . 5
β’ (π β {π‘ β π β£ π΅ β€ (πΉβπ‘)} β (π β π β§ π΅ β€ (πΉβπ ))) |
38 | 27, 37 | bitr4di 289 |
. . . 4
β’ (π β (π β (β‘πΉ β (π΅[,)+β)) β π β {π‘ β π β£ π΅ β€ (πΉβπ‘)})) |
39 | 38 | eqrdv 2731 |
. . 3
β’ (π β (β‘πΉ β (π΅[,)+β)) = {π‘ β π β£ π΅ β€ (πΉβπ‘)}) |
40 | | rfcnpre3.5 |
. . 3
β’ π΄ = {π‘ β π β£ π΅ β€ (πΉβπ‘)} |
41 | 39, 40 | eqtr4di 2791 |
. 2
β’ (π β (β‘πΉ β (π΅[,)+β)) = π΄) |
42 | | icopnfcld 24147 |
. . . . 5
β’ (π΅ β β β (π΅[,)+β) β
(Clsdβ(topGenβran (,)))) |
43 | 9, 42 | syl 17 |
. . . 4
β’ (π β (π΅[,)+β) β
(Clsdβ(topGenβran (,)))) |
44 | 1 | fveq2i 6846 |
. . . 4
β’
(ClsdβπΎ) =
(Clsdβ(topGenβran (,))) |
45 | 43, 44 | eleqtrrdi 2845 |
. . 3
β’ (π β (π΅[,)+β) β (ClsdβπΎ)) |
46 | | cnclima 22635 |
. . 3
β’ ((πΉ β (π½ Cn πΎ) β§ (π΅[,)+β) β (ClsdβπΎ)) β (β‘πΉ β (π΅[,)+β)) β (Clsdβπ½)) |
47 | 4, 45, 46 | syl2anc 585 |
. 2
β’ (π β (β‘πΉ β (π΅[,)+β)) β (Clsdβπ½)) |
48 | 41, 47 | eqeltrrd 2835 |
1
β’ (π β π΄ β (Clsdβπ½)) |