Step | Hyp | Ref
| Expression |
1 | | xkohmeo.f |
. . 3
|
2 | | xkohmeo.x |
. . . . . . 7
TopOn |
3 | | xkohmeo.y |
. . . . . . 7
TopOn |
4 | | txtopon 21394 |
. . . . . . 7
TopOn TopOn
TopOn |
5 | 2, 3, 4 | syl2anc 693 |
. . . . . 6
TopOn
|
6 | | topontop 20718 |
. . . . . 6
TopOn |
7 | 5, 6 | syl 17 |
. . . . 5
|
8 | | xkohmeo.l |
. . . . 5
|
9 | | eqid 2622 |
. . . . . 6
|
10 | 9 | xkotopon 21403 |
. . . . 5
TopOn |
11 | 7, 8, 10 | syl2anc 693 |
. . . 4
TopOn |
12 | | vex 3203 |
. . . . . . . . 9
|
13 | | vex 3203 |
. . . . . . . . 9
|
14 | 12, 13 | op1std 7178 |
. . . . . . . 8
|
15 | 12, 13 | op2ndd 7179 |
. . . . . . . 8
|
16 | | eqidd 2623 |
. . . . . . . 8
|
17 | 14, 15, 16 | oveq123d 6671 |
. . . . . . 7
|
18 | 17 | mpteq2dv 4745 |
. . . . . 6
|
19 | 18 | mpt2mpt 6752 |
. . . . 5
|
20 | | txtopon 21394 |
. . . . . . 7
TopOn
TopOn TopOn |
21 | 11, 2, 20 | syl2anc 693 |
. . . . . 6
TopOn |
22 | | vex 3203 |
. . . . . . . . . . 11
|
23 | | vex 3203 |
. . . . . . . . . . 11
|
24 | 22, 23 | op1std 7178 |
. . . . . . . . . 10
|
25 | 24 | fveq2d 6195 |
. . . . . . . . 9
|
26 | 24 | fveq2d 6195 |
. . . . . . . . 9
|
27 | 22, 23 | op2ndd 7179 |
. . . . . . . . 9
|
28 | 25, 26, 27 | oveq123d 6671 |
. . . . . . . 8
|
29 | 28 | mpt2mpt 6752 |
. . . . . . 7
|
30 | | txtopon 21394 |
. . . . . . . . 9
TopOn TopOn TopOn |
31 | 21, 3, 30 | syl2anc 693 |
. . . . . . . 8
TopOn |
32 | | eqid 2622 |
. . . . . . . . . 10
|
33 | 32 | toptopon 20722 |
. . . . . . . . 9
TopOn |
34 | 8, 33 | sylib 208 |
. . . . . . . 8
TopOn |
35 | | xkohmeo.j |
. . . . . . . . 9
𝑛Locally |
36 | | xkohmeo.k |
. . . . . . . . 9
𝑛Locally |
37 | | txcmp 21446 |
. . . . . . . . . 10
|
38 | 37 | txnlly 21440 |
. . . . . . . . 9
𝑛Locally
𝑛Locally 𝑛Locally |
39 | 35, 36, 38 | syl2anc 693 |
. . . . . . . 8
𝑛Locally |
40 | 25 | mpt2mpt 6752 |
. . . . . . . . . 10
|
41 | 5 | adantr 481 |
. . . . . . . . . . . . 13
TopOn |
42 | 34 | adantr 481 |
. . . . . . . . . . . . 13
TopOn |
43 | | xp1st 7198 |
. . . . . . . . . . . . . . 15
|
44 | 43 | adantl 482 |
. . . . . . . . . . . . . 14
|
45 | | xp1st 7198 |
. . . . . . . . . . . . . 14
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . 13
|
47 | | cnf2 21053 |
. . . . . . . . . . . . 13
TopOn
TopOn |
48 | 41, 42, 46, 47 | syl3anc 1326 |
. . . . . . . . . . . 12
|
49 | 48 | feqmptd 6249 |
. . . . . . . . . . 11
|
50 | 49 | mpteq2dva 4744 |
. . . . . . . . . 10
|
51 | 40, 50 | syl5eqr 2670 |
. . . . . . . . 9
|
52 | 21, 3 | cnmpt1st 21471 |
. . . . . . . . . 10
|
53 | | fveq2 6191 |
. . . . . . . . . . . 12
|
54 | 53 | cbvmptv 4750 |
. . . . . . . . . . 11
|
55 | 14 | mpt2mpt 6752 |
. . . . . . . . . . . 12
|
56 | 11, 2 | cnmpt1st 21471 |
. . . . . . . . . . . 12
|
57 | 55, 56 | syl5eqel 2705 |
. . . . . . . . . . 11
|
58 | 54, 57 | syl5eqel 2705 |
. . . . . . . . . 10
|
59 | 21, 3, 52, 21, 58, 53 | cnmpt21 21474 |
. . . . . . . . 9
|
60 | 51, 59 | eqeltrrd 2702 |
. . . . . . . 8
|
61 | 26 | mpt2mpt 6752 |
. . . . . . . . . 10
|
62 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
63 | 62 | cbvmptv 4750 |
. . . . . . . . . . . 12
|
64 | 15 | mpt2mpt 6752 |
. . . . . . . . . . . . 13
|
65 | 11, 2 | cnmpt2nd 21472 |
. . . . . . . . . . . . 13
|
66 | 64, 65 | syl5eqel 2705 |
. . . . . . . . . . . 12
|
67 | 63, 66 | syl5eqel 2705 |
. . . . . . . . . . 11
|
68 | 21, 3, 52, 21, 67, 62 | cnmpt21 21474 |
. . . . . . . . . 10
|
69 | 61, 68 | syl5eqel 2705 |
. . . . . . . . 9
|
70 | 27 | mpt2mpt 6752 |
. . . . . . . . . 10
|
71 | 21, 3 | cnmpt2nd 21472 |
. . . . . . . . . 10
|
72 | 70, 71 | syl5eqel 2705 |
. . . . . . . . 9
|
73 | 31, 69, 72 | cnmpt1t 21468 |
. . . . . . . 8
|
74 | | fveq2 6191 |
. . . . . . . . 9
|
75 | | df-ov 6653 |
. . . . . . . . 9
|
76 | 74, 75 | syl6eqr 2674 |
. . . . . . . 8
|
77 | 31, 5, 34, 39, 60, 73, 76 | cnmptk1p 21488 |
. . . . . . 7
|
78 | 29, 77 | syl5eqelr 2706 |
. . . . . 6
|
79 | 21, 3, 78 | cnmpt2k 21491 |
. . . . 5
|
80 | 19, 79 | syl5eqelr 2706 |
. . . 4
|
81 | 11, 2, 80 | cnmpt2k 21491 |
. . 3
|
82 | 1, 81 | syl5eqel 2705 |
. 2
|
83 | 2, 3, 1, 35, 36, 8 | xkocnv 21617 |
. . . 4
|
84 | 13, 23 | op1std 7178 |
. . . . . . . 8
|
85 | 84 | fveq2d 6195 |
. . . . . . 7
|
86 | 13, 23 | op2ndd 7179 |
. . . . . . 7
|
87 | 85, 86 | fveq12d 6197 |
. . . . . 6
|
88 | 87 | mpt2mpt 6752 |
. . . . 5
|
89 | 88 | mpteq2i 4741 |
. . . 4
|
90 | 83, 89 | syl6eqr 2674 |
. . 3
|
91 | | nllytop 21276 |
. . . . . 6
𝑛Locally |
92 | 35, 91 | syl 17 |
. . . . 5
|
93 | | nllytop 21276 |
. . . . . . 7
𝑛Locally |
94 | 36, 93 | syl 17 |
. . . . . 6
|
95 | | xkotop 21391 |
. . . . . 6
|
96 | 94, 8, 95 | syl2anc 693 |
. . . . 5
|
97 | | eqid 2622 |
. . . . . 6
|
98 | 97 | xkotopon 21403 |
. . . . 5
TopOn |
99 | 92, 96, 98 | syl2anc 693 |
. . . 4
TopOn
|
100 | | vex 3203 |
. . . . . . . . 9
|
101 | 100, 22 | op1std 7178 |
. . . . . . . 8
|
102 | 100, 22 | op2ndd 7179 |
. . . . . . . . 9
|
103 | 102 | fveq2d 6195 |
. . . . . . . 8
|
104 | 101, 103 | fveq12d 6197 |
. . . . . . 7
|
105 | 102 | fveq2d 6195 |
. . . . . . 7
|
106 | 104, 105 | fveq12d 6197 |
. . . . . 6
|
107 | 106 | mpt2mpt 6752 |
. . . . 5
|
108 | | txtopon 21394 |
. . . . . . 7
TopOn
TopOn
TopOn |
109 | 99, 5, 108 | syl2anc 693 |
. . . . . 6
TopOn |
110 | 3 | adantr 481 |
. . . . . . . . . 10
TopOn |
111 | 34 | adantr 481 |
. . . . . . . . . 10
TopOn |
112 | 2 | adantr 481 |
. . . . . . . . . . . 12
TopOn |
113 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
114 | 113 | xkotopon 21403 |
. . . . . . . . . . . . . 14
TopOn |
115 | 94, 8, 114 | syl2anc 693 |
. . . . . . . . . . . . 13
TopOn |
116 | 115 | adantr 481 |
. . . . . . . . . . . 12
TopOn |
117 | | xp1st 7198 |
. . . . . . . . . . . . 13
|
118 | 117 | adantl 482 |
. . . . . . . . . . . 12
|
119 | | cnf2 21053 |
. . . . . . . . . . . 12
TopOn TopOn
|
120 | 112, 116,
118, 119 | syl3anc 1326 |
. . . . . . . . . . 11
|
121 | | xp2nd 7199 |
. . . . . . . . . . . . 13
|
122 | 121 | adantl 482 |
. . . . . . . . . . . 12
|
123 | | xp1st 7198 |
. . . . . . . . . . . 12
|
124 | 122, 123 | syl 17 |
. . . . . . . . . . 11
|
125 | 120, 124 | ffvelrnd 6360 |
. . . . . . . . . 10
|
126 | | cnf2 21053 |
. . . . . . . . . 10
TopOn TopOn |
127 | 110, 111,
125, 126 | syl3anc 1326 |
. . . . . . . . 9
|
128 | 127 | feqmptd 6249 |
. . . . . . . 8
|
129 | 128 | mpteq2dva 4744 |
. . . . . . 7
|
130 | 101 | mpt2mpt 6752 |
. . . . . . . . . 10
|
131 | 120 | feqmptd 6249 |
. . . . . . . . . . 11
|
132 | 131 | mpteq2dva 4744 |
. . . . . . . . . 10
|
133 | 130, 132 | syl5eqr 2670 |
. . . . . . . . 9
|
134 | 99, 5 | cnmpt1st 21471 |
. . . . . . . . 9
|
135 | 133, 134 | eqeltrrd 2702 |
. . . . . . . 8
|
136 | 103 | mpt2mpt 6752 |
. . . . . . . . 9
|
137 | 99, 5 | cnmpt2nd 21472 |
. . . . . . . . . 10
|
138 | 53 | cbvmptv 4750 |
. . . . . . . . . . 11
|
139 | 84 | mpt2mpt 6752 |
. . . . . . . . . . . 12
|
140 | 2, 3 | cnmpt1st 21471 |
. . . . . . . . . . . 12
|
141 | 139, 140 | syl5eqel 2705 |
. . . . . . . . . . 11
|
142 | 138, 141 | syl5eqel 2705 |
. . . . . . . . . 10
|
143 | 99, 5, 137, 5, 142, 53 | cnmpt21 21474 |
. . . . . . . . 9
|
144 | 136, 143 | syl5eqel 2705 |
. . . . . . . 8
|
145 | | fveq2 6191 |
. . . . . . . 8
|
146 | 109, 2, 115, 35, 135, 144, 145 | cnmptk1p 21488 |
. . . . . . 7
|
147 | 129, 146 | eqeltrrd 2702 |
. . . . . 6
|
148 | 105 | mpt2mpt 6752 |
. . . . . . 7
|
149 | 62 | cbvmptv 4750 |
. . . . . . . . 9
|
150 | 86 | mpt2mpt 6752 |
. . . . . . . . . 10
|
151 | 2, 3 | cnmpt2nd 21472 |
. . . . . . . . . 10
|
152 | 150, 151 | syl5eqel 2705 |
. . . . . . . . 9
|
153 | 149, 152 | syl5eqel 2705 |
. . . . . . . 8
|
154 | 99, 5, 137, 5, 153, 62 | cnmpt21 21474 |
. . . . . . 7
|
155 | 148, 154 | syl5eqel 2705 |
. . . . . 6
|
156 | | fveq2 6191 |
. . . . . 6
|
157 | 109, 3, 34, 36, 147, 155, 156 | cnmptk1p 21488 |
. . . . 5
|
158 | 107, 157 | syl5eqelr 2706 |
. . . 4
|
159 | 99, 5, 158 | cnmpt2k 21491 |
. . 3
|
160 | 90, 159 | eqeltrd 2701 |
. 2
|
161 | | ishmeo 21562 |
. 2
|
162 | 82, 160, 161 | sylanbrc 698 |
1
|