Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . . 7
|
2 | | df-ov 6653 |
. . . . . . 7
|
3 | 1, 2 | syl6eqr 2674 |
. . . . . 6
|
4 | | fveq2 6191 |
. . . . . . 7
|
5 | | df-ov 6653 |
. . . . . . 7
|
6 | 4, 5 | syl6eqr 2674 |
. . . . . 6
|
7 | 3, 6 | opeq12d 4410 |
. . . . 5
|
8 | 7 | mpt2mpt 6752 |
. . . 4
|
9 | | nfcv 2764 |
. . . . . . 7
|
10 | | nfmpt21 6722 |
. . . . . . 7
|
11 | | nfcv 2764 |
. . . . . . 7
|
12 | 9, 10, 11 | nfov 6676 |
. . . . . 6
|
13 | | nfmpt21 6722 |
. . . . . . 7
|
14 | 9, 13, 11 | nfov 6676 |
. . . . . 6
|
15 | 12, 14 | nfop 4418 |
. . . . 5
|
16 | | nfcv 2764 |
. . . . . . 7
|
17 | | nfmpt22 6723 |
. . . . . . 7
|
18 | | nfcv 2764 |
. . . . . . 7
|
19 | 16, 17, 18 | nfov 6676 |
. . . . . 6
|
20 | | nfmpt22 6723 |
. . . . . . 7
|
21 | 16, 20, 18 | nfov 6676 |
. . . . . 6
|
22 | 19, 21 | nfop 4418 |
. . . . 5
|
23 | | nfcv 2764 |
. . . . 5
|
24 | | nfcv 2764 |
. . . . 5
|
25 | | oveq12 6659 |
. . . . . 6
|
26 | | oveq12 6659 |
. . . . . 6
|
27 | 25, 26 | opeq12d 4410 |
. . . . 5
|
28 | 15, 22, 23, 24, 27 | cbvmpt2 6734 |
. . . 4
|
29 | 8, 28 | eqtri 2644 |
. . 3
|
30 | | cnmpt21.j |
. . . . 5
TopOn |
31 | | cnmpt21.k |
. . . . 5
TopOn |
32 | | txtopon 21394 |
. . . . 5
TopOn TopOn
TopOn |
33 | 30, 31, 32 | syl2anc 693 |
. . . 4
TopOn
|
34 | | toponuni 20719 |
. . . 4
TopOn
|
35 | | mpteq1 4737 |
. . . 4
|
36 | 33, 34, 35 | 3syl 18 |
. . 3
|
37 | | simp2 1062 |
. . . . . 6
|
38 | | simp3 1063 |
. . . . . 6
|
39 | | cnmpt21.a |
. . . . . . . . . . . 12
|
40 | | cntop2 21045 |
. . . . . . . . . . . 12
|
41 | 39, 40 | syl 17 |
. . . . . . . . . . 11
|
42 | | eqid 2622 |
. . . . . . . . . . . 12
|
43 | 42 | toptopon 20722 |
. . . . . . . . . . 11
TopOn |
44 | 41, 43 | sylib 208 |
. . . . . . . . . 10
TopOn |
45 | | cnf2 21053 |
. . . . . . . . . 10
TopOn
TopOn |
46 | 33, 44, 39, 45 | syl3anc 1326 |
. . . . . . . . 9
|
47 | | eqid 2622 |
. . . . . . . . . 10
|
48 | 47 | fmpt2 7237 |
. . . . . . . . 9
|
49 | 46, 48 | sylibr 224 |
. . . . . . . 8
|
50 | | rsp2 2936 |
. . . . . . . 8
|
51 | 49, 50 | syl 17 |
. . . . . . 7
|
52 | 51 | 3impib 1262 |
. . . . . 6
|
53 | 47 | ovmpt4g 6783 |
. . . . . 6
|
54 | 37, 38, 52, 53 | syl3anc 1326 |
. . . . 5
|
55 | | cnmpt2t.b |
. . . . . . . . . . . 12
|
56 | | cntop2 21045 |
. . . . . . . . . . . 12
|
57 | 55, 56 | syl 17 |
. . . . . . . . . . 11
|
58 | | eqid 2622 |
. . . . . . . . . . . 12
|
59 | 58 | toptopon 20722 |
. . . . . . . . . . 11
TopOn |
60 | 57, 59 | sylib 208 |
. . . . . . . . . 10
TopOn |
61 | | cnf2 21053 |
. . . . . . . . . 10
TopOn
TopOn |
62 | 33, 60, 55, 61 | syl3anc 1326 |
. . . . . . . . 9
|
63 | | eqid 2622 |
. . . . . . . . . 10
|
64 | 63 | fmpt2 7237 |
. . . . . . . . 9
|
65 | 62, 64 | sylibr 224 |
. . . . . . . 8
|
66 | | rsp2 2936 |
. . . . . . . 8
|
67 | 65, 66 | syl 17 |
. . . . . . 7
|
68 | 67 | 3impib 1262 |
. . . . . 6
|
69 | 63 | ovmpt4g 6783 |
. . . . . 6
|
70 | 37, 38, 68, 69 | syl3anc 1326 |
. . . . 5
|
71 | 54, 70 | opeq12d 4410 |
. . . 4
|
72 | 71 | mpt2eq3dva 6719 |
. . 3
|
73 | 29, 36, 72 | 3eqtr3a 2680 |
. 2
|
74 | | eqid 2622 |
. . . 4
|
75 | | eqid 2622 |
. . . 4
|
76 | 74, 75 | txcnmpt 21427 |
. . 3
|
77 | 39, 55, 76 | syl2anc 693 |
. 2
|
78 | 73, 77 | eqeltrrd 2702 |
1
|