Step | Hyp | Ref
| Expression |
1 | | fveq2 5483 |
. . . . . . 7
|
2 | | df-ov 5842 |
. . . . . . 7
|
3 | 1, 2 | eqtr4di 2215 |
. . . . . 6
|
4 | | fveq2 5483 |
. . . . . . 7
|
5 | | df-ov 5842 |
. . . . . . 7
|
6 | 4, 5 | eqtr4di 2215 |
. . . . . 6
|
7 | 3, 6 | opeq12d 3763 |
. . . . 5
|
8 | 7 | mpompt 5928 |
. . . 4
|
9 | | nfcv 2306 |
. . . . . . 7
|
10 | | nfmpo1 5903 |
. . . . . . 7
|
11 | | nfcv 2306 |
. . . . . . 7
|
12 | 9, 10, 11 | nfov 5866 |
. . . . . 6
|
13 | | nfmpo1 5903 |
. . . . . . 7
|
14 | 9, 13, 11 | nfov 5866 |
. . . . . 6
|
15 | 12, 14 | nfop 3771 |
. . . . 5
|
16 | | nfcv 2306 |
. . . . . . 7
|
17 | | nfmpo2 5904 |
. . . . . . 7
|
18 | | nfcv 2306 |
. . . . . . 7
|
19 | 16, 17, 18 | nfov 5866 |
. . . . . 6
|
20 | | nfmpo2 5904 |
. . . . . . 7
|
21 | 16, 20, 18 | nfov 5866 |
. . . . . 6
|
22 | 19, 21 | nfop 3771 |
. . . . 5
|
23 | | nfcv 2306 |
. . . . 5
|
24 | | nfcv 2306 |
. . . . 5
|
25 | | oveq12 5848 |
. . . . . 6
|
26 | | oveq12 5848 |
. . . . . 6
|
27 | 25, 26 | opeq12d 3763 |
. . . . 5
|
28 | 15, 22, 23, 24, 27 | cbvmpo 5915 |
. . . 4
|
29 | 8, 28 | eqtri 2185 |
. . 3
|
30 | | cnmpt21.j |
. . . . 5
TopOn |
31 | | cnmpt21.k |
. . . . 5
TopOn |
32 | | txtopon 12860 |
. . . . 5
TopOn TopOn
TopOn |
33 | 30, 31, 32 | syl2anc 409 |
. . . 4
TopOn
|
34 | | toponuni 12611 |
. . . 4
TopOn
|
35 | | mpteq1 4063 |
. . . 4
|
36 | 33, 34, 35 | 3syl 17 |
. . 3
|
37 | | simp2 987 |
. . . . . 6
|
38 | | simp3 988 |
. . . . . 6
|
39 | | cnmpt21.a |
. . . . . . . . . . . 12
|
40 | | cntop2 12800 |
. . . . . . . . . . . 12
|
41 | 39, 40 | syl 14 |
. . . . . . . . . . 11
|
42 | | toptopon2 12615 |
. . . . . . . . . . 11
TopOn |
43 | 41, 42 | sylib 121 |
. . . . . . . . . 10
TopOn |
44 | | cnf2 12803 |
. . . . . . . . . 10
TopOn
TopOn |
45 | 33, 43, 39, 44 | syl3anc 1227 |
. . . . . . . . 9
|
46 | | eqid 2164 |
. . . . . . . . . 10
|
47 | 46 | fmpo 6164 |
. . . . . . . . 9
|
48 | 45, 47 | sylibr 133 |
. . . . . . . 8
|
49 | | rsp2 2514 |
. . . . . . . 8
|
50 | 48, 49 | syl 14 |
. . . . . . 7
|
51 | 50 | 3impib 1190 |
. . . . . 6
|
52 | 46 | ovmpt4g 5958 |
. . . . . 6
|
53 | 37, 38, 51, 52 | syl3anc 1227 |
. . . . 5
|
54 | | cnmpt2t.b |
. . . . . . . . . . . 12
|
55 | | cntop2 12800 |
. . . . . . . . . . . 12
|
56 | 54, 55 | syl 14 |
. . . . . . . . . . 11
|
57 | | toptopon2 12615 |
. . . . . . . . . . 11
TopOn |
58 | 56, 57 | sylib 121 |
. . . . . . . . . 10
TopOn |
59 | | cnf2 12803 |
. . . . . . . . . 10
TopOn
TopOn |
60 | 33, 58, 54, 59 | syl3anc 1227 |
. . . . . . . . 9
|
61 | | eqid 2164 |
. . . . . . . . . 10
|
62 | 61 | fmpo 6164 |
. . . . . . . . 9
|
63 | 60, 62 | sylibr 133 |
. . . . . . . 8
|
64 | | rsp2 2514 |
. . . . . . . 8
|
65 | 63, 64 | syl 14 |
. . . . . . 7
|
66 | 65 | 3impib 1190 |
. . . . . 6
|
67 | 61 | ovmpt4g 5958 |
. . . . . 6
|
68 | 37, 38, 66, 67 | syl3anc 1227 |
. . . . 5
|
69 | 53, 68 | opeq12d 3763 |
. . . 4
|
70 | 69 | mpoeq3dva 5900 |
. . 3
|
71 | 29, 36, 70 | 3eqtr3a 2221 |
. 2
|
72 | | eqid 2164 |
. . . 4
|
73 | | eqid 2164 |
. . . 4
|
74 | 72, 73 | txcnmpt 12871 |
. . 3
|
75 | 39, 54, 74 | syl2anc 409 |
. 2
|
76 | 71, 75 | eqeltrrd 2242 |
1
|