Step | Hyp | Ref
| Expression |
1 | | rfcnpre1.3 |
. . . 4
β’
β²π₯π |
2 | | rfcnpre1.2 |
. . . . . 6
β’
β²π₯πΉ |
3 | 2 | nfcnv 5876 |
. . . . 5
β’
β²π₯β‘πΉ |
4 | | rfcnpre1.1 |
. . . . . 6
β’
β²π₯π΅ |
5 | | nfcv 2903 |
. . . . . 6
β’
β²π₯(,) |
6 | | nfcv 2903 |
. . . . . 6
β’
β²π₯+β |
7 | 4, 5, 6 | nfov 7435 |
. . . . 5
β’
β²π₯(π΅(,)+β) |
8 | 3, 7 | nfima 6065 |
. . . 4
β’
β²π₯(β‘πΉ β (π΅(,)+β)) |
9 | | nfrab1 3451 |
. . . 4
β’
β²π₯{π₯ β π β£ π΅ < (πΉβπ₯)} |
10 | | rfcnpre1.8 |
. . . . . . . . . 10
β’ (π β πΉ β (π½ Cn πΎ)) |
11 | | cntop1 22735 |
. . . . . . . . . . . . 13
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π½ β Top) |
13 | | rfcnpre1.5 |
. . . . . . . . . . . 12
β’ π = βͺ
π½ |
14 | | istopon 22405 |
. . . . . . . . . . . 12
β’ (π½ β (TopOnβπ) β (π½ β Top β§ π = βͺ π½)) |
15 | 12, 13, 14 | sylanblrc 590 |
. . . . . . . . . . 11
β’ (π β π½ β (TopOnβπ)) |
16 | | rfcnpre1.4 |
. . . . . . . . . . . 12
β’ πΎ = (topGenβran
(,)) |
17 | | retopon 24271 |
. . . . . . . . . . . 12
β’
(topGenβran (,)) β (TopOnββ) |
18 | 16, 17 | eqeltri 2829 |
. . . . . . . . . . 11
β’ πΎ β
(TopOnββ) |
19 | | iscn 22730 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnββ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆβ β§ βπ¦ β πΎ (β‘πΉ β π¦) β π½))) |
20 | 15, 18, 19 | sylancl 586 |
. . . . . . . . . 10
β’ (π β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆβ β§ βπ¦ β πΎ (β‘πΉ β π¦) β π½))) |
21 | 10, 20 | mpbid 231 |
. . . . . . . . 9
β’ (π β (πΉ:πβΆβ β§ βπ¦ β πΎ (β‘πΉ β π¦) β π½)) |
22 | 21 | simpld 495 |
. . . . . . . 8
β’ (π β πΉ:πβΆβ) |
23 | 22 | ffvelcdmda 7083 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (πΉβπ₯) β β) |
24 | | rfcnpre1.7 |
. . . . . . . . 9
β’ (π β π΅ β
β*) |
25 | | elioopnf 13416 |
. . . . . . . . 9
β’ (π΅ β β*
β ((πΉβπ₯) β (π΅(,)+β) β ((πΉβπ₯) β β β§ π΅ < (πΉβπ₯)))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
β’ (π β ((πΉβπ₯) β (π΅(,)+β) β ((πΉβπ₯) β β β§ π΅ < (πΉβπ₯)))) |
27 | 26 | baibd 540 |
. . . . . . 7
β’ ((π β§ (πΉβπ₯) β β) β ((πΉβπ₯) β (π΅(,)+β) β π΅ < (πΉβπ₯))) |
28 | 23, 27 | syldan 591 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((πΉβπ₯) β (π΅(,)+β) β π΅ < (πΉβπ₯))) |
29 | 28 | pm5.32da 579 |
. . . . 5
β’ (π β ((π₯ β π β§ (πΉβπ₯) β (π΅(,)+β)) β (π₯ β π β§ π΅ < (πΉβπ₯)))) |
30 | | ffn 6714 |
. . . . . 6
β’ (πΉ:πβΆβ β πΉ Fn π) |
31 | | elpreima 7056 |
. . . . . 6
β’ (πΉ Fn π β (π₯ β (β‘πΉ β (π΅(,)+β)) β (π₯ β π β§ (πΉβπ₯) β (π΅(,)+β)))) |
32 | 22, 30, 31 | 3syl 18 |
. . . . 5
β’ (π β (π₯ β (β‘πΉ β (π΅(,)+β)) β (π₯ β π β§ (πΉβπ₯) β (π΅(,)+β)))) |
33 | | rabid 3452 |
. . . . . 6
β’ (π₯ β {π₯ β π β£ π΅ < (πΉβπ₯)} β (π₯ β π β§ π΅ < (πΉβπ₯))) |
34 | 33 | a1i 11 |
. . . . 5
β’ (π β (π₯ β {π₯ β π β£ π΅ < (πΉβπ₯)} β (π₯ β π β§ π΅ < (πΉβπ₯)))) |
35 | 29, 32, 34 | 3bitr4d 310 |
. . . 4
β’ (π β (π₯ β (β‘πΉ β (π΅(,)+β)) β π₯ β {π₯ β π β£ π΅ < (πΉβπ₯)})) |
36 | 1, 8, 9, 35 | eqrd 4000 |
. . 3
β’ (π β (β‘πΉ β (π΅(,)+β)) = {π₯ β π β£ π΅ < (πΉβπ₯)}) |
37 | | rfcnpre1.6 |
. . 3
β’ π΄ = {π₯ β π β£ π΅ < (πΉβπ₯)} |
38 | 36, 37 | eqtr4di 2790 |
. 2
β’ (π β (β‘πΉ β (π΅(,)+β)) = π΄) |
39 | | iooretop 24273 |
. . . 4
β’ (π΅(,)+β) β
(topGenβran (,)) |
40 | 39, 16 | eleqtrri 2832 |
. . 3
β’ (π΅(,)+β) β πΎ |
41 | | cnima 22760 |
. . 3
β’ ((πΉ β (π½ Cn πΎ) β§ (π΅(,)+β) β πΎ) β (β‘πΉ β (π΅(,)+β)) β π½) |
42 | 10, 40, 41 | sylancl 586 |
. 2
β’ (π β (β‘πΉ β (π΅(,)+β)) β π½) |
43 | 38, 42 | eqeltrrd 2834 |
1
β’ (π β π΄ β π½) |