Step | Hyp | Ref
| Expression |
1 | | cncfuni.f |
. . 3
|
2 | | cncfuni.auni |
. . . . . . 7
|
3 | 2 | sselda 3603 |
. . . . . 6
|
4 | | eluni2 4440 |
. . . . . 6
|
5 | 3, 4 | sylib 208 |
. . . . 5
|
6 | | simp1l 1085 |
. . . . . . 7
|
7 | | simp2 1062 |
. . . . . . 7
|
8 | | elin 3796 |
. . . . . . . . . 10
|
9 | 8 | biimpri 218 |
. . . . . . . . 9
|
10 | 9 | adantll 750 |
. . . . . . . 8
|
11 | 10 | 3adant2 1080 |
. . . . . . 7
|
12 | | cncfuni.fcn |
. . . . . . . . . . . . . 14
|
13 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . 21
|
14 | 1, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
15 | 14 | ineq2d 3814 |
. . . . . . . . . . . . . . . . . . 19
|
16 | | incom 3805 |
. . . . . . . . . . . . . . . . . . 19
|
17 | 15, 16 | syl6req 2673 |
. . . . . . . . . . . . . . . . . 18
|
18 | 17 | reseq2d 5396 |
. . . . . . . . . . . . . . . . 17
|
19 | | frel 6050 |
. . . . . . . . . . . . . . . . . . 19
|
20 | 1, 19 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
21 | | resindm 5444 |
. . . . . . . . . . . . . . . . . 18
|
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
|
23 | 18, 22 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
|
24 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . 20
|
25 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
26 | | cncfuni.acn |
. . . . . . . . . . . . . . . . . . 19
|
27 | 25, 26 | sstrd 3613 |
. . . . . . . . . . . . . . . . . 18
|
28 | | ssid 3624 |
. . . . . . . . . . . . . . . . . . 19
|
29 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
30 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
ℂfld ℂfld |
31 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
ℂfld ↾t ℂfld
↾t |
32 | 30 | cnfldtop 22587 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld |
33 | | unicntop 22589 |
. . . . . . . . . . . . . . . . . . . . . 22
ℂfld |
34 | 33 | restid 16094 |
. . . . . . . . . . . . . . . . . . . . 21
ℂfld ℂfld
↾t ℂfld |
35 | 32, 34 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld ↾t ℂfld |
36 | 35 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . 19
ℂfld ℂfld ↾t |
37 | 30, 31, 36 | cncfcn 22712 |
. . . . . . . . . . . . . . . . . 18
ℂfld
↾t ℂfld |
38 | 27, 29, 37 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
ℂfld ↾t ℂfld |
39 | 38 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
ℂfld ↾t ℂfld |
40 | 23, 39 | eleq12d 2695 |
. . . . . . . . . . . . . . 15
ℂfld
↾t ℂfld
|
41 | 40 | adantr 481 |
. . . . . . . . . . . . . 14
ℂfld ↾t ℂfld
|
42 | 12, 41 | mpbird 247 |
. . . . . . . . . . . . 13
ℂfld ↾t ℂfld |
43 | 42 | 3adant3 1081 |
. . . . . . . . . . . 12
ℂfld
↾t ℂfld |
44 | 30 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . 16
ℂfld TopOn |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . 15
ℂfld
TopOn |
46 | | resttopon 20965 |
. . . . . . . . . . . . . . 15
ℂfld
TopOn
ℂfld ↾t TopOn |
47 | 45, 27, 46 | syl2anc 693 |
. . . . . . . . . . . . . 14
ℂfld
↾t TopOn |
48 | 47 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
ℂfld ↾t TopOn |
49 | 44 | a1i 11 |
. . . . . . . . . . . . 13
ℂfld TopOn |
50 | | cncnp 21084 |
. . . . . . . . . . . . 13
ℂfld
↾t TopOn ℂfld
TopOn
ℂfld
↾t ℂfld
ℂfld ↾t ℂfld |
51 | 48, 49, 50 | syl2anc 693 |
. . . . . . . . . . . 12
ℂfld ↾t ℂfld
ℂfld ↾t ℂfld |
52 | 43, 51 | mpbid 222 |
. . . . . . . . . . 11
ℂfld ↾t ℂfld |
53 | 52 | simprd 479 |
. . . . . . . . . 10
ℂfld ↾t ℂfld |
54 | | simp3 1063 |
. . . . . . . . . 10
|
55 | | rspa 2930 |
. . . . . . . . . 10
ℂfld
↾t ℂfld
ℂfld ↾t ℂfld |
56 | 53, 54, 55 | syl2anc 693 |
. . . . . . . . 9
ℂfld ↾t ℂfld |
57 | 32 | a1i 11 |
. . . . . . . . . . . . . 14
ℂfld
|
58 | | cnex 10017 |
. . . . . . . . . . . . . . . 16
|
59 | 58 | ssex 4802 |
. . . . . . . . . . . . . . 15
|
60 | 26, 59 | syl 17 |
. . . . . . . . . . . . . 14
|
61 | | restabs 20969 |
. . . . . . . . . . . . . 14
ℂfld
ℂfld ↾t ↾t ℂfld
↾t |
62 | 57, 25, 60, 61 | syl3anc 1326 |
. . . . . . . . . . . . 13
ℂfld ↾t ↾t ℂfld
↾t |
63 | 62 | eqcomd 2628 |
. . . . . . . . . . . 12
ℂfld
↾t ℂfld ↾t ↾t |
64 | 63 | oveq1d 6665 |
. . . . . . . . . . 11
ℂfld ↾t ℂfld ℂfld ↾t ↾t ℂfld |
65 | 64 | fveq1d 6193 |
. . . . . . . . . 10
ℂfld ↾t ℂfld ℂfld ↾t ↾t ℂfld |
66 | 65 | 3ad2ant1 1082 |
. . . . . . . . 9
ℂfld
↾t ℂfld ℂfld ↾t ↾t ℂfld |
67 | 56, 66 | eleqtrd 2703 |
. . . . . . . 8
ℂfld ↾t
↾t ℂfld |
68 | | resttop 20964 |
. . . . . . . . . . 11
ℂfld
ℂfld
↾t |
69 | 57, 60, 68 | syl2anc 693 |
. . . . . . . . . 10
ℂfld
↾t |
70 | 69 | 3ad2ant1 1082 |
. . . . . . . . 9
ℂfld ↾t |
71 | 33 | restuni 20966 |
. . . . . . . . . . . 12
ℂfld
ℂfld
↾t |
72 | 57, 26, 71 | syl2anc 693 |
. . . . . . . . . . 11
ℂfld
↾t |
73 | 25, 72 | sseqtrd 3641 |
. . . . . . . . . 10
ℂfld
↾t |
74 | 73 | 3ad2ant1 1082 |
. . . . . . . . 9
ℂfld
↾t |
75 | | cncfuni.opn |
. . . . . . . . . . . . 13
ℂfld
↾t |
76 | 75 | 3adant3 1081 |
. . . . . . . . . . . 12
ℂfld
↾t |
77 | | eqid 2622 |
. . . . . . . . . . . . . 14
ℂfld
↾t ℂfld
↾t |
78 | 77 | isopn3 20870 |
. . . . . . . . . . . . 13
ℂfld
↾t
ℂfld
↾t ℂfld
↾t
ℂfld ↾t |
79 | 70, 74, 78 | syl2anc 693 |
. . . . . . . . . . . 12
ℂfld
↾t
ℂfld ↾t |
80 | 76, 79 | mpbid 222 |
. . . . . . . . . . 11
ℂfld ↾t |
81 | 80 | eqcomd 2628 |
. . . . . . . . . 10
ℂfld
↾t
|
82 | 54, 81 | eleqtrd 2703 |
. . . . . . . . 9
ℂfld
↾t
|
83 | 72 | feq2d 6031 |
. . . . . . . . . . 11
ℂfld
↾t |
84 | 1, 83 | mpbid 222 |
. . . . . . . . . 10
ℂfld
↾t |
85 | 84 | 3ad2ant1 1082 |
. . . . . . . . 9
ℂfld
↾t |
86 | 77, 33 | cnprest 21093 |
. . . . . . . . 9
ℂfld ↾t
ℂfld
↾t
ℂfld
↾t
ℂfld ↾t ℂfld ↾t ℂfld
ℂfld ↾t
↾t ℂfld |
87 | 70, 74, 82, 85, 86 | syl22anc 1327 |
. . . . . . . 8
ℂfld ↾t ℂfld
ℂfld ↾t
↾t ℂfld |
88 | 67, 87 | mpbird 247 |
. . . . . . 7
ℂfld ↾t ℂfld |
89 | 6, 7, 11, 88 | syl3anc 1326 |
. . . . . 6
ℂfld ↾t ℂfld |
90 | 89 | rexlimdv3a 3033 |
. . . . 5
ℂfld
↾t ℂfld |
91 | 5, 90 | mpd 15 |
. . . 4
ℂfld ↾t ℂfld |
92 | 91 | ralrimiva 2966 |
. . 3
ℂfld
↾t ℂfld |
93 | | resttopon 20965 |
. . . . 5
ℂfld
TopOn ℂfld
↾t TopOn |
94 | 45, 26, 93 | syl2anc 693 |
. . . 4
ℂfld
↾t TopOn |
95 | | cncnp 21084 |
. . . 4
ℂfld
↾t TopOn ℂfld TopOn
ℂfld
↾t ℂfld
ℂfld ↾t ℂfld |
96 | 94, 45, 95 | syl2anc 693 |
. . 3
ℂfld
↾t ℂfld
ℂfld ↾t ℂfld |
97 | 1, 92, 96 | mpbir2and 957 |
. 2
ℂfld
↾t ℂfld |
98 | | eqid 2622 |
. . . . 5
ℂfld ↾t ℂfld
↾t |
99 | 30, 98, 36 | cncfcn 22712 |
. . . 4
ℂfld
↾t ℂfld |
100 | 26, 29, 99 | syl2anc 693 |
. . 3
ℂfld ↾t ℂfld |
101 | 100 | eqcomd 2628 |
. 2
ℂfld ↾t ℂfld |
102 | 97, 101 | eleqtrd 2703 |
1
|