Step | Hyp | Ref
| Expression |
1 | | df-ov 6653 |
. . . . . . . . . 10
|
2 | | simprl 794 |
. . . . . . . . . . 11
|
3 | | simprr 796 |
. . . . . . . . . . 11
|
4 | | cnmpt21.j |
. . . . . . . . . . . . . . . 16
TopOn |
5 | | cnmpt21.k |
. . . . . . . . . . . . . . . 16
TopOn |
6 | | txtopon 21394 |
. . . . . . . . . . . . . . . 16
TopOn TopOn
TopOn |
7 | 4, 5, 6 | syl2anc 693 |
. . . . . . . . . . . . . . 15
TopOn
|
8 | | cnmpt21.l |
. . . . . . . . . . . . . . 15
TopOn |
9 | | cnmpt21.a |
. . . . . . . . . . . . . . 15
|
10 | | cnf2 21053 |
. . . . . . . . . . . . . . 15
TopOn
TopOn
|
11 | 7, 8, 9, 10 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
12 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
13 | 12 | fmpt2 7237 |
. . . . . . . . . . . . . 14
|
14 | 11, 13 | sylibr 224 |
. . . . . . . . . . . . 13
|
15 | | rsp2 2936 |
. . . . . . . . . . . . 13
|
16 | 14, 15 | syl 17 |
. . . . . . . . . . . 12
|
17 | 16 | imp 445 |
. . . . . . . . . . 11
|
18 | 12 | ovmpt4g 6783 |
. . . . . . . . . . 11
|
19 | 2, 3, 17, 18 | syl3anc 1326 |
. . . . . . . . . 10
|
20 | 1, 19 | syl5eqr 2670 |
. . . . . . . . 9
|
21 | 20 | fveq2d 6195 |
. . . . . . . 8
|
22 | | cnmpt21.b |
. . . . . . . . . . . . . . 15
|
23 | | cntop2 21045 |
. . . . . . . . . . . . . . 15
|
24 | 22, 23 | syl 17 |
. . . . . . . . . . . . . 14
|
25 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
26 | 25 | toptopon 20722 |
. . . . . . . . . . . . . 14
TopOn |
27 | 24, 26 | sylib 208 |
. . . . . . . . . . . . 13
TopOn |
28 | | cnf2 21053 |
. . . . . . . . . . . . 13
TopOn TopOn |
29 | 8, 27, 22, 28 | syl3anc 1326 |
. . . . . . . . . . . 12
|
30 | | eqid 2622 |
. . . . . . . . . . . . 13
|
31 | 30 | fmpt 6381 |
. . . . . . . . . . . 12
|
32 | 29, 31 | sylibr 224 |
. . . . . . . . . . 11
|
33 | 32 | adantr 481 |
. . . . . . . . . 10
|
34 | | cnmpt21.c |
. . . . . . . . . . . 12
|
35 | 34 | eleq1d 2686 |
. . . . . . . . . . 11
|
36 | 35 | rspcv 3305 |
. . . . . . . . . 10
|
37 | 17, 33, 36 | sylc 65 |
. . . . . . . . 9
|
38 | 34, 30 | fvmptg 6280 |
. . . . . . . . 9
|
39 | 17, 37, 38 | syl2anc 693 |
. . . . . . . 8
|
40 | 21, 39 | eqtrd 2656 |
. . . . . . 7
|
41 | | opelxpi 5148 |
. . . . . . . 8
|
42 | | fvco3 6275 |
. . . . . . . 8
|
43 | 11, 41, 42 | syl2an 494 |
. . . . . . 7
|
44 | | df-ov 6653 |
. . . . . . . 8
|
45 | | eqid 2622 |
. . . . . . . . . 10
|
46 | 45 | ovmpt4g 6783 |
. . . . . . . . 9
|
47 | 2, 3, 37, 46 | syl3anc 1326 |
. . . . . . . 8
|
48 | 44, 47 | syl5eqr 2670 |
. . . . . . 7
|
49 | 40, 43, 48 | 3eqtr4d 2666 |
. . . . . 6
|
50 | 49 | ralrimivva 2971 |
. . . . 5
|
51 | | nfv 1843 |
. . . . . 6
|
52 | | nfcv 2764 |
. . . . . . 7
|
53 | | nfcv 2764 |
. . . . . . . . . 10
|
54 | | nfmpt21 6722 |
. . . . . . . . . 10
|
55 | 53, 54 | nfco 5287 |
. . . . . . . . 9
|
56 | | nfcv 2764 |
. . . . . . . . 9
|
57 | 55, 56 | nffv 6198 |
. . . . . . . 8
|
58 | | nfmpt21 6722 |
. . . . . . . . 9
|
59 | 58, 56 | nffv 6198 |
. . . . . . . 8
|
60 | 57, 59 | nfeq 2776 |
. . . . . . 7
|
61 | 52, 60 | nfral 2945 |
. . . . . 6
|
62 | | nfv 1843 |
. . . . . . . 8
|
63 | | nfcv 2764 |
. . . . . . . . . . 11
|
64 | | nfmpt22 6723 |
. . . . . . . . . . 11
|
65 | 63, 64 | nfco 5287 |
. . . . . . . . . 10
|
66 | | nfcv 2764 |
. . . . . . . . . 10
|
67 | 65, 66 | nffv 6198 |
. . . . . . . . 9
|
68 | | nfmpt22 6723 |
. . . . . . . . . 10
|
69 | 68, 66 | nffv 6198 |
. . . . . . . . 9
|
70 | 67, 69 | nfeq 2776 |
. . . . . . . 8
|
71 | | opeq2 4403 |
. . . . . . . . . 10
|
72 | 71 | fveq2d 6195 |
. . . . . . . . 9
|
73 | 71 | fveq2d 6195 |
. . . . . . . . 9
|
74 | 72, 73 | eqeq12d 2637 |
. . . . . . . 8
|
75 | 62, 70, 74 | cbvral 3167 |
. . . . . . 7
|
76 | | opeq1 4402 |
. . . . . . . . . 10
|
77 | 76 | fveq2d 6195 |
. . . . . . . . 9
|
78 | 76 | fveq2d 6195 |
. . . . . . . . 9
|
79 | 77, 78 | eqeq12d 2637 |
. . . . . . . 8
|
80 | 79 | ralbidv 2986 |
. . . . . . 7
|
81 | 75, 80 | syl5bb 272 |
. . . . . 6
|
82 | 51, 61, 81 | cbvral 3167 |
. . . . 5
|
83 | 50, 82 | sylib 208 |
. . . 4
|
84 | | fveq2 6191 |
. . . . . 6
|
85 | | fveq2 6191 |
. . . . . 6
|
86 | 84, 85 | eqeq12d 2637 |
. . . . 5
|
87 | 86 | ralxp 5263 |
. . . 4
|
88 | 83, 87 | sylibr 224 |
. . 3
|
89 | | fco 6058 |
. . . . . 6
|
90 | 29, 11, 89 | syl2anc 693 |
. . . . 5
|
91 | | ffn 6045 |
. . . . 5
|
92 | 90, 91 | syl 17 |
. . . 4
|
93 | 37 | ralrimivva 2971 |
. . . . . 6
|
94 | 45 | fmpt2 7237 |
. . . . . 6
|
95 | 93, 94 | sylib 208 |
. . . . 5
|
96 | | ffn 6045 |
. . . . 5
|
97 | 95, 96 | syl 17 |
. . . 4
|
98 | | eqfnfv 6311 |
. . . 4
|
99 | 92, 97, 98 | syl2anc 693 |
. . 3
|
100 | 88, 99 | mpbird 247 |
. 2
|
101 | | cnco 21070 |
. . 3
|
102 | 9, 22, 101 | syl2anc 693 |
. 2
|
103 | 100, 102 | eqeltrrd 2702 |
1
|