Step | Hyp | Ref
| Expression |
1 | | cnextf.3 |
. . . 4
|
2 | | cnextf.4 |
. . . 4
|
3 | | cnextf.5 |
. . . 4
|
4 | | cnextf.a |
. . . 4
|
5 | | cnextf.1 |
. . . . 5
|
6 | | cnextf.2 |
. . . . 5
|
7 | 5, 6 | cnextfun 21868 |
. . . 4
CnExt |
8 | 1, 2, 3, 4, 7 | syl22anc 1327 |
. . 3
CnExt |
9 | | simpl 473 |
. . . . . . 7
|
10 | | cnextf.6 |
. . . . . . . . 9
|
11 | 10 | eleq2d 2687 |
. . . . . . . 8
|
12 | 11 | biimpar 502 |
. . . . . . 7
|
13 | | cnextf.7 |
. . . . . . . 8
↾t |
14 | | n0 3931 |
. . . . . . . 8
↾t
↾t |
15 | 13, 14 | sylib 208 |
. . . . . . 7
↾t |
16 | | haustop 21135 |
. . . . . . . . . . . . . 14
|
17 | 2, 16 | syl 17 |
. . . . . . . . . . . . 13
|
18 | 5, 6 | cnextfval 21866 |
. . . . . . . . . . . . 13
CnExt
↾t |
19 | 1, 17, 3, 4, 18 | syl22anc 1327 |
. . . . . . . . . . . 12
CnExt
↾t |
20 | 19 | eleq2d 2687 |
. . . . . . . . . . 11
CnExt
↾t |
21 | | opeliunxp 5170 |
. . . . . . . . . . 11
↾t
↾t |
22 | 20, 21 | syl6bb 276 |
. . . . . . . . . 10
CnExt
↾t |
23 | 22 | exbidv 1850 |
. . . . . . . . 9
CnExt
↾t |
24 | | 19.42v 1918 |
. . . . . . . . 9
↾t
↾t |
25 | 23, 24 | syl6bb 276 |
. . . . . . . 8
CnExt
↾t |
26 | 25 | biimpar 502 |
. . . . . . 7
↾t CnExt |
27 | 9, 12, 15, 26 | syl12anc 1324 |
. . . . . 6
CnExt |
28 | 25 | simprbda 653 |
. . . . . . 7
CnExt
|
29 | 11 | adantr 481 |
. . . . . . 7
CnExt
|
30 | 28, 29 | mpbid 222 |
. . . . . 6
CnExt
|
31 | 27, 30 | impbida 877 |
. . . . 5
CnExt |
32 | 31 | abbi2dv 2742 |
. . . 4
CnExt |
33 | | dfdm3 5310 |
. . . 4
CnExt CnExt |
34 | 32, 33 | syl6reqr 2675 |
. . 3
CnExt |
35 | | df-fn 5891 |
. . 3
CnExt CnExt CnExt |
36 | 8, 34, 35 | sylanbrc 698 |
. 2
CnExt |
37 | 19 | rneqd 5353 |
. . 3
CnExt
↾t |
38 | | rniun 5543 |
. . . 4
↾t
↾t |
39 | | vex 3203 |
. . . . . . . . 9
|
40 | 39 | snnz 4309 |
. . . . . . . 8
|
41 | | rnxp 5564 |
. . . . . . . 8
↾t
↾t |
42 | 40, 41 | ax-mp 5 |
. . . . . . 7
↾t
↾t |
43 | 11 | biimpa 501 |
. . . . . . . 8
|
44 | 6 | toptopon 20722 |
. . . . . . . . . . 11
TopOn |
45 | 17, 44 | sylib 208 |
. . . . . . . . . 10
TopOn |
46 | 45 | adantr 481 |
. . . . . . . . 9
TopOn |
47 | 5 | toptopon 20722 |
. . . . . . . . . . . 12
TopOn |
48 | 1, 47 | sylib 208 |
. . . . . . . . . . 11
TopOn |
49 | 48 | adantr 481 |
. . . . . . . . . 10
TopOn |
50 | 4 | adantr 481 |
. . . . . . . . . 10
|
51 | | simpr 477 |
. . . . . . . . . 10
|
52 | | trnei 21696 |
. . . . . . . . . . 11
TopOn
↾t |
53 | 52 | biimpa 501 |
. . . . . . . . . 10
TopOn
↾t |
54 | 49, 50, 51, 12, 53 | syl31anc 1329 |
. . . . . . . . 9
↾t |
55 | 3 | adantr 481 |
. . . . . . . . 9
|
56 | | flfelbas 21798 |
. . . . . . . . . . 11
TopOn
↾t
↾t |
57 | 56 | ex 450 |
. . . . . . . . . 10
TopOn
↾t
↾t |
58 | 57 | ssrdv 3609 |
. . . . . . . . 9
TopOn
↾t
↾t |
59 | 46, 54, 55, 58 | syl3anc 1326 |
. . . . . . . 8
↾t |
60 | 43, 59 | syldan 487 |
. . . . . . 7
↾t |
61 | 42, 60 | syl5eqss 3649 |
. . . . . 6
↾t |
62 | 61 | ralrimiva 2966 |
. . . . 5
↾t |
63 | | iunss 4561 |
. . . . 5
↾t
↾t |
64 | 62, 63 | sylibr 224 |
. . . 4
↾t |
65 | 38, 64 | syl5eqss 3649 |
. . 3
↾t |
66 | 37, 65 | eqsstrd 3639 |
. 2
CnExt
|
67 | | df-f 5892 |
. 2
CnExt
CnExt CnExt |
68 | 36, 66, 67 | sylanbrc 698 |
1
CnExt |