Step | Hyp | Ref
| Expression |
1 | | simp31 1097 |
. . . . . 6
|
2 | | cncff 22696 |
. . . . . 6
|
3 | 1, 2 | syl 17 |
. . . . 5
|
4 | | ffun 6048 |
. . . . 5
|
5 | 3, 4 | syl 17 |
. . . 4
|
6 | 5 | 3ad2ant3 1084 |
. . 3
|
7 | | iccconn 22633 |
. . . . . . . . 9
↾t Conn |
8 | 7 | 3adant3 1081 |
. . . . . . . 8
↾t Conn |
9 | 8 | 3ad2ant1 1082 |
. . . . . . 7
↾t Conn |
10 | | simpr1 1067 |
. . . . . . . . . . . . . 14
|
11 | 10, 2 | syl 17 |
. . . . . . . . . . . . 13
|
12 | 11 | anim2i 593 |
. . . . . . . . . . . 12
|
13 | 12 | 3impb 1260 |
. . . . . . . . . . 11
|
14 | 13 | 3ad2ant3 1084 |
. . . . . . . . . 10
|
15 | 4 | adantl 482 |
. . . . . . . . . . 11
|
16 | | fdm 6051 |
. . . . . . . . . . . . 13
|
17 | 16 | sseq2d 3633 |
. . . . . . . . . . . 12
|
18 | 17 | biimparc 504 |
. . . . . . . . . . 11
|
19 | 15, 18 | jca 554 |
. . . . . . . . . 10
|
20 | 14, 19 | syl 17 |
. . . . . . . . 9
|
21 | | fores 6124 |
. . . . . . . . 9
|
22 | 20, 21 | syl 17 |
. . . . . . . 8
|
23 | | retop 22565 |
. . . . . . . . . 10
|
24 | | simp332 1215 |
. . . . . . . . . 10
|
25 | | uniretop 22566 |
. . . . . . . . . . 11
|
26 | 25 | restuni 20966 |
. . . . . . . . . 10
↾t |
27 | 23, 24, 26 | sylancr 695 |
. . . . . . . . 9
↾t |
28 | | foeq3 6113 |
. . . . . . . . 9
↾t ↾t |
29 | 27, 28 | syl 17 |
. . . . . . . 8
↾t |
30 | 22, 29 | mpbid 222 |
. . . . . . 7
↾t |
31 | | simp331 1214 |
. . . . . . . . . . . 12
|
32 | | ssid 3624 |
. . . . . . . . . . . . . . 15
|
33 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
ℂfld ℂfld |
34 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
ℂfld ↾t ℂfld
↾t |
35 | 33 | cnfldtop 22587 |
. . . . . . . . . . . . . . . . . 18
ℂfld |
36 | 33 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld TopOn |
37 | 36 | toponunii 20721 |
. . . . . . . . . . . . . . . . . . 19
ℂfld |
38 | 37 | restid 16094 |
. . . . . . . . . . . . . . . . . 18
ℂfld ℂfld
↾t ℂfld |
39 | 35, 38 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
ℂfld ↾t ℂfld |
40 | 39 | eqcomi 2631 |
. . . . . . . . . . . . . . . 16
ℂfld ℂfld ↾t |
41 | 33, 34, 40 | cncfcn 22712 |
. . . . . . . . . . . . . . 15
ℂfld
↾t ℂfld |
42 | 32, 41 | mpan2 707 |
. . . . . . . . . . . . . 14
ℂfld
↾t ℂfld |
43 | 42 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
ℂfld
↾t ℂfld |
44 | 43 | 3ad2ant3 1084 |
. . . . . . . . . . . 12
ℂfld ↾t ℂfld |
45 | 31, 44 | eleqtrd 2703 |
. . . . . . . . . . 11
ℂfld
↾t ℂfld |
46 | | simp31 1097 |
. . . . . . . . . . . 12
|
47 | | simp32 1098 |
. . . . . . . . . . . . . 14
|
48 | | resttopon 20965 |
. . . . . . . . . . . . . 14
ℂfld
TopOn ℂfld
↾t TopOn |
49 | 36, 47, 48 | sylancr 695 |
. . . . . . . . . . . . 13
ℂfld
↾t TopOn |
50 | | toponuni 20719 |
. . . . . . . . . . . . 13
ℂfld
↾t TopOn ℂfld ↾t |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . 12
ℂfld
↾t |
52 | 46, 51 | sseqtrd 3641 |
. . . . . . . . . . 11
ℂfld
↾t |
53 | | eqid 2622 |
. . . . . . . . . . . 12
ℂfld
↾t ℂfld
↾t |
54 | 53 | cnrest 21089 |
. . . . . . . . . . 11
ℂfld
↾t ℂfld ℂfld
↾t ℂfld
↾t
↾t ℂfld |
55 | 45, 52, 54 | syl2anc 693 |
. . . . . . . . . 10
ℂfld
↾t
↾t ℂfld |
56 | 35 | a1i 11 |
. . . . . . . . . . . . 13
ℂfld
|
57 | | cnex 10017 |
. . . . . . . . . . . . . 14
|
58 | | ssexg 4804 |
. . . . . . . . . . . . . 14
|
59 | 47, 57, 58 | sylancl 694 |
. . . . . . . . . . . . 13
|
60 | | restabs 20969 |
. . . . . . . . . . . . 13
ℂfld
ℂfld ↾t ↾t ℂfld
↾t |
61 | 56, 46, 59, 60 | syl3anc 1326 |
. . . . . . . . . . . 12
ℂfld ↾t ↾t ℂfld
↾t |
62 | | iccssre 12255 |
. . . . . . . . . . . . . . 15
|
63 | 62 | 3adant3 1081 |
. . . . . . . . . . . . . 14
|
64 | 63 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
|
65 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
66 | 33, 65 | rerest 22607 |
. . . . . . . . . . . . 13
ℂfld ↾t ↾t |
67 | 64, 66 | syl 17 |
. . . . . . . . . . . 12
ℂfld
↾t ↾t |
68 | 61, 67 | eqtrd 2656 |
. . . . . . . . . . 11
ℂfld ↾t ↾t ↾t |
69 | 68 | oveq1d 6665 |
. . . . . . . . . 10
ℂfld ↾t
↾t ℂfld ↾t ℂfld |
70 | 55, 69 | eleqtrd 2703 |
. . . . . . . . 9
↾t ℂfld |
71 | 36 | a1i 11 |
. . . . . . . . . 10
ℂfld
TopOn |
72 | | df-ima 5127 |
. . . . . . . . . . . 12
|
73 | 72 | eqimss2i 3660 |
. . . . . . . . . . 11
|
74 | 73 | a1i 11 |
. . . . . . . . . 10
|
75 | | ax-resscn 9993 |
. . . . . . . . . . 11
|
76 | 24, 75 | syl6ss 3615 |
. . . . . . . . . 10
|
77 | | cnrest2 21090 |
. . . . . . . . . 10
ℂfld
TopOn
↾t ℂfld
↾t ℂfld
↾t |
78 | 71, 74, 76, 77 | syl3anc 1326 |
. . . . . . . . 9
↾t ℂfld
↾t ℂfld
↾t |
79 | 70, 78 | mpbid 222 |
. . . . . . . 8
↾t ℂfld ↾t |
80 | 33, 65 | rerest 22607 |
. . . . . . . . . 10
ℂfld ↾t ↾t |
81 | 24, 80 | syl 17 |
. . . . . . . . 9
ℂfld
↾t ↾t |
82 | 81 | oveq2d 6666 |
. . . . . . . 8
↾t ℂfld
↾t ↾t
↾t |
83 | 79, 82 | eleqtrd 2703 |
. . . . . . 7
↾t
↾t |
84 | | eqid 2622 |
. . . . . . . 8
↾t ↾t |
85 | 84 | cnconn 21225 |
. . . . . . 7
↾t Conn
↾t ↾t
↾t
↾t Conn |
86 | 9, 30, 83, 85 | syl3anc 1326 |
. . . . . 6
↾t Conn |
87 | | reconn 22631 |
. . . . . . . . 9
↾t Conn
|
88 | 87 | 3ad2ant2 1083 |
. . . . . . . 8
↾t Conn
|
89 | 88 | 3ad2ant3 1084 |
. . . . . . 7
↾t Conn
|
90 | 89 | 3ad2ant3 1084 |
. . . . . 6
↾t Conn
|
91 | 86, 90 | mpbid 222 |
. . . . 5
|
92 | | simp11 1091 |
. . . . . . . . 9
|
93 | 92 | rexrd 10089 |
. . . . . . . 8
|
94 | | simp12 1092 |
. . . . . . . . 9
|
95 | 94 | rexrd 10089 |
. . . . . . . 8
|
96 | | ltle 10126 |
. . . . . . . . . . 11
|
97 | 96 | imp 445 |
. . . . . . . . . 10
|
98 | 97 | 3adantl3 1219 |
. . . . . . . . 9
|
99 | 98 | 3adant3 1081 |
. . . . . . . 8
|
100 | | lbicc2 12288 |
. . . . . . . 8
|
101 | 93, 95, 99, 100 | syl3anc 1326 |
. . . . . . 7
|
102 | | funfvima2 6493 |
. . . . . . 7
|
103 | 20, 101, 102 | sylc 65 |
. . . . . 6
|
104 | | ubicc2 12289 |
. . . . . . . 8
|
105 | 93, 95, 99, 104 | syl3anc 1326 |
. . . . . . 7
|
106 | | funfvima2 6493 |
. . . . . . 7
|
107 | 20, 105, 106 | sylc 65 |
. . . . . 6
|
108 | | oveq1 6657 |
. . . . . . . 8
|
109 | 108 | sseq1d 3632 |
. . . . . . 7
|
110 | | oveq2 6658 |
. . . . . . . 8
|
111 | 110 | sseq1d 3632 |
. . . . . . 7
|
112 | 109, 111 | rspc2v 3322 |
. . . . . 6
|
113 | 103, 107,
112 | syl2anc 693 |
. . . . 5
|
114 | 91, 113 | mpd 15 |
. . . 4
|
115 | | ioossicc 12259 |
. . . . . . . 8
|
116 | 115 | sseli 3599 |
. . . . . . 7
|
117 | 116 | 3ad2ant3 1084 |
. . . . . 6
|
118 | 117 | 3ad2ant3 1084 |
. . . . 5
|
119 | 118 | 3ad2ant3 1084 |
. . . 4
|
120 | 114, 119 | sseldd 3604 |
. . 3
|
121 | | fvelima 6248 |
. . 3
|
122 | 6, 120, 121 | syl2anc 693 |
. 2
|
123 | | simpl1 1064 |
. . . . . . . 8
|
124 | 123 | a1i 11 |
. . . . . . 7
|
125 | | simprr 796 |
. . . . . . . . . . . 12
|
126 | 24, 103 | sseldd 3604 |
. . . . . . . . . . . . . 14
|
127 | | simp333 1216 |
. . . . . . . . . . . . . . . 16
|
128 | 126 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
|
129 | 24, 107 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
|
130 | 129 | rexrd 10089 |
. . . . . . . . . . . . . . . . 17
|
131 | | elioo2 12216 |
. . . . . . . . . . . . . . . . 17
|
132 | 128, 130,
131 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
133 | 127, 132 | mpbid 222 |
. . . . . . . . . . . . . . 15
|
134 | 133 | simp2d 1074 |
. . . . . . . . . . . . . 14
|
135 | 126, 134 | gtned 10172 |
. . . . . . . . . . . . 13
|
136 | 135 | adantr 481 |
. . . . . . . . . . . 12
|
137 | 125, 136 | eqnetrd 2861 |
. . . . . . . . . . 11
|
138 | 137 | neneqd 2799 |
. . . . . . . . . 10
|
139 | | fveq2 6191 |
. . . . . . . . . 10
|
140 | 138, 139 | nsyl 135 |
. . . . . . . . 9
|
141 | | simp13 1093 |
. . . . . . . . . . . . . 14
|
142 | 133 | simp3d 1075 |
. . . . . . . . . . . . . 14
|
143 | 141, 142 | ltned 10173 |
. . . . . . . . . . . . 13
|
144 | 143 | adantr 481 |
. . . . . . . . . . . 12
|
145 | 125, 144 | eqnetrd 2861 |
. . . . . . . . . . 11
|
146 | 145 | neneqd 2799 |
. . . . . . . . . 10
|
147 | | fveq2 6191 |
. . . . . . . . . 10
|
148 | 146, 147 | nsyl 135 |
. . . . . . . . 9
|
149 | | simprl3 1108 |
. . . . . . . . 9
|
150 | 140, 148,
149 | ecase13d 32307 |
. . . . . . . 8
|
151 | 150 | ex 450 |
. . . . . . 7
|
152 | 124, 151 | jcad 555 |
. . . . . 6
|
153 | | 3anass 1042 |
. . . . . 6
|
154 | 152, 153 | syl6ibr 242 |
. . . . 5
|
155 | | rexr 10085 |
. . . . . . . . 9
|
156 | | rexr 10085 |
. . . . . . . . 9
|
157 | | elicc3 32311 |
. . . . . . . . 9
|
158 | 155, 156,
157 | syl2an 494 |
. . . . . . . 8
|
159 | 158 | 3adant3 1081 |
. . . . . . 7
|
160 | 159 | 3ad2ant1 1082 |
. . . . . 6
|
161 | 160 | anbi1d 741 |
. . . . 5
|
162 | | elioo1 12215 |
. . . . . . . 8
|
163 | 155, 156,
162 | syl2an 494 |
. . . . . . 7
|
164 | 163 | 3adant3 1081 |
. . . . . 6
|
165 | 164 | 3ad2ant1 1082 |
. . . . 5
|
166 | 154, 161,
165 | 3imtr4d 283 |
. . . 4
|
167 | | simpr 477 |
. . . . 5
|
168 | 167 | a1i 11 |
. . . 4
|
169 | 166, 168 | jcad 555 |
. . 3
|
170 | 169 | reximdv2 3014 |
. 2
|
171 | 122, 170 | mpd 15 |
1
|