Step | Hyp | Ref
| Expression |
1 | | txcnp.4 |
. . . . . 6
TopOn |
2 | | txcnp.5 |
. . . . . 6
TopOn |
3 | | txcnp.8 |
. . . . . 6
|
4 | | cnpf2 12376 |
. . . . . 6
TopOn TopOn
|
5 | 1, 2, 3, 4 | syl3anc 1216 |
. . . . 5
|
6 | 5 | fvmptelrn 5573 |
. . . 4
|
7 | | txcnp.6 |
. . . . . 6
TopOn |
8 | | txcnp.9 |
. . . . . 6
|
9 | | cnpf2 12376 |
. . . . . 6
TopOn TopOn
|
10 | 1, 7, 8, 9 | syl3anc 1216 |
. . . . 5
|
11 | 10 | fvmptelrn 5573 |
. . . 4
|
12 | 6, 11 | opelxpd 4572 |
. . 3
|
13 | 12 | fmpttd 5575 |
. 2
|
14 | | txcnp.7 |
. . . . . . . . 9
|
15 | | simpr 109 |
. . . . . . . . . . . 12
|
16 | 12 | elexd 2699 |
. . . . . . . . . . . 12
|
17 | | eqid 2139 |
. . . . . . . . . . . . 13
|
18 | 17 | fvmpt2 5504 |
. . . . . . . . . . . 12
|
19 | 15, 16, 18 | syl2anc 408 |
. . . . . . . . . . 11
|
20 | | eqid 2139 |
. . . . . . . . . . . . . 14
|
21 | 20 | fvmpt2 5504 |
. . . . . . . . . . . . 13
|
22 | 15, 6, 21 | syl2anc 408 |
. . . . . . . . . . . 12
|
23 | | eqid 2139 |
. . . . . . . . . . . . . 14
|
24 | 23 | fvmpt2 5504 |
. . . . . . . . . . . . 13
|
25 | 15, 11, 24 | syl2anc 408 |
. . . . . . . . . . . 12
|
26 | 22, 25 | opeq12d 3713 |
. . . . . . . . . . 11
|
27 | 19, 26 | eqtr4d 2175 |
. . . . . . . . . 10
|
28 | 27 | ralrimiva 2505 |
. . . . . . . . 9
|
29 | | nffvmpt1 5432 |
. . . . . . . . . . 11
|
30 | | nffvmpt1 5432 |
. . . . . . . . . . . 12
|
31 | | nffvmpt1 5432 |
. . . . . . . . . . . 12
|
32 | 30, 31 | nfop 3721 |
. . . . . . . . . . 11
|
33 | 29, 32 | nfeq 2289 |
. . . . . . . . . 10
|
34 | | fveq2 5421 |
. . . . . . . . . . 11
|
35 | | fveq2 5421 |
. . . . . . . . . . . 12
|
36 | | fveq2 5421 |
. . . . . . . . . . . 12
|
37 | 35, 36 | opeq12d 3713 |
. . . . . . . . . . 11
|
38 | 34, 37 | eqeq12d 2154 |
. . . . . . . . . 10
|
39 | 33, 38 | rspc 2783 |
. . . . . . . . 9
|
40 | 14, 28, 39 | sylc 62 |
. . . . . . . 8
|
41 | 40 | eleq1d 2208 |
. . . . . . 7
|
42 | 41 | adantr 274 |
. . . . . 6
|
43 | 1 | ad2antrr 479 |
. . . . . . . . . 10
TopOn |
44 | 2 | ad2antrr 479 |
. . . . . . . . . 10
TopOn |
45 | 14 | ad2antrr 479 |
. . . . . . . . . 10
|
46 | 3 | ad2antrr 479 |
. . . . . . . . . 10
|
47 | | simplrl 524 |
. . . . . . . . . 10
|
48 | | simprl 520 |
. . . . . . . . . 10
|
49 | | icnpimaex 12380 |
. . . . . . . . . 10
TopOn TopOn
|
50 | 43, 44, 45, 46, 47, 48, 49 | syl33anc 1231 |
. . . . . . . . 9
|
51 | 7 | ad2antrr 479 |
. . . . . . . . . 10
TopOn |
52 | 8 | ad2antrr 479 |
. . . . . . . . . 10
|
53 | | simplrr 525 |
. . . . . . . . . 10
|
54 | | simprr 521 |
. . . . . . . . . 10
|
55 | | icnpimaex 12380 |
. . . . . . . . . 10
TopOn TopOn
|
56 | 43, 51, 45, 52, 53, 54, 55 | syl33anc 1231 |
. . . . . . . . 9
|
57 | 50, 56 | jca 304 |
. . . . . . . 8
|
58 | 57 | ex 114 |
. . . . . . 7
|
59 | | opelxp 4569 |
. . . . . . 7
|
60 | | reeanv 2600 |
. . . . . . 7
|
61 | 58, 59, 60 | 3imtr4g 204 |
. . . . . 6
|
62 | 42, 61 | sylbid 149 |
. . . . 5
|
63 | | an4 575 |
. . . . . . . . . . 11
|
64 | | elin 3259 |
. . . . . . . . . . . . . 14
|
65 | 64 | biimpri 132 |
. . . . . . . . . . . . 13
|
66 | 65 | a1i 9 |
. . . . . . . . . . . 12
|
67 | | simpl 108 |
. . . . . . . . . . . . . . . 16
|
68 | | toponss 12193 |
. . . . . . . . . . . . . . . 16
TopOn |
69 | 1, 67, 68 | syl2an 287 |
. . . . . . . . . . . . . . 15
|
70 | | ssinss1 3305 |
. . . . . . . . . . . . . . . . . . . . 21
|
71 | 70 | adantl 275 |
. . . . . . . . . . . . . . . . . . . 20
|
72 | 71 | sselda 3097 |
. . . . . . . . . . . . . . . . . . 19
|
73 | 28 | ad2antrr 479 |
. . . . . . . . . . . . . . . . . . 19
|
74 | | nffvmpt1 5432 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | | nffvmpt1 5432 |
. . . . . . . . . . . . . . . . . . . . . 22
|
76 | | nffvmpt1 5432 |
. . . . . . . . . . . . . . . . . . . . . 22
|
77 | 75, 76 | nfop 3721 |
. . . . . . . . . . . . . . . . . . . . 21
|
78 | 74, 77 | nfeq 2289 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | | fveq2 5421 |
. . . . . . . . . . . . . . . . . . . . 21
|
80 | | fveq2 5421 |
. . . . . . . . . . . . . . . . . . . . . 22
|
81 | | fveq2 5421 |
. . . . . . . . . . . . . . . . . . . . . 22
|
82 | 80, 81 | opeq12d 3713 |
. . . . . . . . . . . . . . . . . . . . 21
|
83 | 79, 82 | eqeq12d 2154 |
. . . . . . . . . . . . . . . . . . . 20
|
84 | 78, 83 | rspc 2783 |
. . . . . . . . . . . . . . . . . . 19
|
85 | 72, 73, 84 | sylc 62 |
. . . . . . . . . . . . . . . . . 18
|
86 | | simpr 109 |
. . . . . . . . . . . . . . . . . . . . 21
|
87 | 86 | elin1d 3265 |
. . . . . . . . . . . . . . . . . . . 20
|
88 | 5 | ad2antrr 479 |
. . . . . . . . . . . . . . . . . . . . . 22
|
89 | 88 | ffund 5276 |
. . . . . . . . . . . . . . . . . . . . 21
|
90 | 71 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
91 | 88 | fdmd 5279 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
92 | 90, 91 | sseqtrrd 3136 |
. . . . . . . . . . . . . . . . . . . . . 22
|
93 | 92, 86 | sseldd 3098 |
. . . . . . . . . . . . . . . . . . . . 21
|
94 | | funfvima 5649 |
. . . . . . . . . . . . . . . . . . . . 21
|
95 | 89, 93, 94 | syl2anc 408 |
. . . . . . . . . . . . . . . . . . . 20
|
96 | 87, 95 | mpd 13 |
. . . . . . . . . . . . . . . . . . 19
|
97 | 86 | elin2d 3266 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 10 | ad2antrr 479 |
. . . . . . . . . . . . . . . . . . . . . 22
|
99 | 98 | ffund 5276 |
. . . . . . . . . . . . . . . . . . . . 21
|
100 | 98 | fdmd 5279 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
101 | 90, 100 | sseqtrrd 3136 |
. . . . . . . . . . . . . . . . . . . . . 22
|
102 | 101, 86 | sseldd 3098 |
. . . . . . . . . . . . . . . . . . . . 21
|
103 | | funfvima 5649 |
. . . . . . . . . . . . . . . . . . . . 21
|
104 | 99, 102, 103 | syl2anc 408 |
. . . . . . . . . . . . . . . . . . . 20
|
105 | 97, 104 | mpd 13 |
. . . . . . . . . . . . . . . . . . 19
|
106 | 96, 105 | opelxpd 4572 |
. . . . . . . . . . . . . . . . . 18
|
107 | 85, 106 | eqeltrd 2216 |
. . . . . . . . . . . . . . . . 17
|
108 | 107 | ralrimiva 2505 |
. . . . . . . . . . . . . . . 16
|
109 | 13 | ffund 5276 |
. . . . . . . . . . . . . . . . . 18
|
110 | 109 | adantr 274 |
. . . . . . . . . . . . . . . . 17
|
111 | 13 | fdmd 5279 |
. . . . . . . . . . . . . . . . . . 19
|
112 | 111 | adantr 274 |
. . . . . . . . . . . . . . . . . 18
|
113 | 71, 112 | sseqtrrd 3136 |
. . . . . . . . . . . . . . . . 17
|
114 | | funimass4 5472 |
. . . . . . . . . . . . . . . . 17
|
115 | 110, 113,
114 | syl2anc 408 |
. . . . . . . . . . . . . . . 16
|
116 | 108, 115 | mpbird 166 |
. . . . . . . . . . . . . . 15
|
117 | 69, 116 | syldan 280 |
. . . . . . . . . . . . . 14
|
118 | 117 | adantlr 468 |
. . . . . . . . . . . . 13
|
119 | | xpss12 4646 |
. . . . . . . . . . . . 13
|
120 | | sstr2 3104 |
. . . . . . . . . . . . 13
|
121 | 118, 119,
120 | syl2im 38 |
. . . . . . . . . . . 12
|
122 | 66, 121 | anim12d 333 |
. . . . . . . . . . 11
|
123 | 63, 122 | syl5bi 151 |
. . . . . . . . . 10
|
124 | | topontop 12181 |
. . . . . . . . . . . . 13
TopOn
|
125 | 1, 124 | syl 14 |
. . . . . . . . . . . 12
|
126 | | inopn 12170 |
. . . . . . . . . . . . 13
|
127 | 126 | 3expb 1182 |
. . . . . . . . . . . 12
|
128 | 125, 127 | sylan 281 |
. . . . . . . . . . 11
|
129 | 128 | adantlr 468 |
. . . . . . . . . 10
|
130 | 123, 129 | jctild 314 |
. . . . . . . . 9
|
131 | 130 | expimpd 360 |
. . . . . . . 8
|
132 | | eleq2 2203 |
. . . . . . . . . 10
|
133 | | imaeq2 4877 |
. . . . . . . . . . 11
|
134 | 133 | sseq1d 3126 |
. . . . . . . . . 10
|
135 | 132, 134 | anbi12d 464 |
. . . . . . . . 9
|
136 | 135 | rspcev 2789 |
. . . . . . . 8
|
137 | 131, 136 | syl6 33 |
. . . . . . 7
|
138 | 137 | expd 256 |
. . . . . 6
|
139 | 138 | rexlimdvv 2556 |
. . . . 5
|
140 | 62, 139 | syld 45 |
. . . 4
|
141 | 140 | ralrimivva 2514 |
. . 3
|
142 | | vex 2689 |
. . . . . 6
|
143 | | vex 2689 |
. . . . . 6
|
144 | 142, 143 | xpex 4654 |
. . . . 5
|
145 | 144 | rgen2w 2488 |
. . . 4
|
146 | | eqid 2139 |
. . . . 5
|
147 | | eleq2 2203 |
. . . . . 6
|
148 | | sseq2 3121 |
. . . . . . . 8
|
149 | 148 | anbi2d 459 |
. . . . . . 7
|
150 | 149 | rexbidv 2438 |
. . . . . 6
|
151 | 147, 150 | imbi12d 233 |
. . . . 5
|
152 | 146, 151 | ralrnmpo 5885 |
. . . 4
|
153 | 145, 152 | ax-mp 5 |
. . 3
|
154 | 141, 153 | sylibr 133 |
. 2
|
155 | | topontop 12181 |
. . . . 5
TopOn
|
156 | 2, 155 | syl 14 |
. . . 4
|
157 | | topontop 12181 |
. . . . 5
TopOn
|
158 | 7, 157 | syl 14 |
. . . 4
|
159 | | eqid 2139 |
. . . . 5
|
160 | 159 | txval 12424 |
. . . 4
|
161 | 156, 158,
160 | syl2anc 408 |
. . 3
|
162 | | txtopon 12431 |
. . . 4
TopOn TopOn
TopOn |
163 | 2, 7, 162 | syl2anc 408 |
. . 3
TopOn
|
164 | 1, 161, 163, 14 | tgcnp 12378 |
. 2
|
165 | 13, 154, 164 | mpbir2and 928 |
1
|