Proof of Theorem xkocnv
Step | Hyp | Ref
| Expression |
1 | | simprr 796 |
. . . . . 6
|
2 | | xkohmeo.x |
. . . . . . . . 9
TopOn |
3 | 2 | adantr 481 |
. . . . . . . 8
TopOn |
4 | | xkohmeo.y |
. . . . . . . . 9
TopOn |
5 | 4 | adantr 481 |
. . . . . . . 8
TopOn |
6 | | txtopon 21394 |
. . . . . . . . . . . . . 14
TopOn TopOn
TopOn |
7 | 2, 4, 6 | syl2anc 693 |
. . . . . . . . . . . . 13
TopOn
|
8 | 7 | adantr 481 |
. . . . . . . . . . . 12
TopOn |
9 | | xkohmeo.l |
. . . . . . . . . . . . . 14
|
10 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
11 | 10 | toptopon 20722 |
. . . . . . . . . . . . . 14
TopOn |
12 | 9, 11 | sylib 208 |
. . . . . . . . . . . . 13
TopOn |
13 | 12 | adantr 481 |
. . . . . . . . . . . 12
TopOn |
14 | | simpr 477 |
. . . . . . . . . . . 12
|
15 | | cnf2 21053 |
. . . . . . . . . . . 12
TopOn
TopOn
|
16 | 8, 13, 14, 15 | syl3anc 1326 |
. . . . . . . . . . 11
|
17 | | ffn 6045 |
. . . . . . . . . . 11
|
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
|
19 | | fnov 6768 |
. . . . . . . . . 10
|
20 | 18, 19 | sylib 208 |
. . . . . . . . 9
|
21 | 20, 14 | eqeltrrd 2702 |
. . . . . . . 8
|
22 | 3, 5, 21 | cnmpt2k 21491 |
. . . . . . 7
|
23 | 22 | adantrr 753 |
. . . . . 6
|
24 | 1, 23 | eqeltrd 2701 |
. . . . 5
|
25 | 20 | adantrr 753 |
. . . . . 6
|
26 | | eqid 2622 |
. . . . . . 7
|
27 | | nfv 1843 |
. . . . . . . . 9
|
28 | | nfv 1843 |
. . . . . . . . . 10
|
29 | | nfmpt1 4747 |
. . . . . . . . . . 11
|
30 | 29 | nfeq2 2780 |
. . . . . . . . . 10
|
31 | 28, 30 | nfan 1828 |
. . . . . . . . 9
|
32 | 27, 31 | nfan 1828 |
. . . . . . . 8
|
33 | | nfv 1843 |
. . . . . . . . . . . . 13
|
34 | | nfv 1843 |
. . . . . . . . . . . . . 14
|
35 | | nfcv 2764 |
. . . . . . . . . . . . . . . 16
|
36 | | nfmpt1 4747 |
. . . . . . . . . . . . . . . 16
|
37 | 35, 36 | nfmpt 4746 |
. . . . . . . . . . . . . . 15
|
38 | 37 | nfeq2 2780 |
. . . . . . . . . . . . . 14
|
39 | 34, 38 | nfan 1828 |
. . . . . . . . . . . . 13
|
40 | 33, 39 | nfan 1828 |
. . . . . . . . . . . 12
|
41 | | nfv 1843 |
. . . . . . . . . . . 12
|
42 | 40, 41 | nfan 1828 |
. . . . . . . . . . 11
|
43 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
|
45 | | simprl 794 |
. . . . . . . . . . . . . . . 16
|
46 | | toponmax 20730 |
. . . . . . . . . . . . . . . . . . 19
TopOn
|
47 | 4, 46 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
48 | 47 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
|
49 | | mptexg 6484 |
. . . . . . . . . . . . . . . . 17
|
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
|
51 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
52 | 51 | fvmpt2 6291 |
. . . . . . . . . . . . . . . 16
|
53 | 45, 50, 52 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
54 | 44, 53 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
55 | 54 | fveq1d 6193 |
. . . . . . . . . . . . 13
|
56 | | simprr 796 |
. . . . . . . . . . . . . 14
|
57 | | ovex 6678 |
. . . . . . . . . . . . . 14
|
58 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
59 | 58 | fvmpt2 6291 |
. . . . . . . . . . . . . 14
|
60 | 56, 57, 59 | sylancl 694 |
. . . . . . . . . . . . 13
|
61 | 55, 60 | eqtrd 2656 |
. . . . . . . . . . . 12
|
62 | 61 | expr 643 |
. . . . . . . . . . 11
|
63 | 42, 62 | ralrimi 2957 |
. . . . . . . . . 10
|
64 | | eqid 2622 |
. . . . . . . . . 10
|
65 | 63, 64 | jctil 560 |
. . . . . . . . 9
|
66 | 65 | ex 450 |
. . . . . . . 8
|
67 | 32, 66 | ralrimi 2957 |
. . . . . . 7
|
68 | | mpt2eq123 6714 |
. . . . . . 7
|
69 | 26, 67, 68 | sylancr 695 |
. . . . . 6
|
70 | 25, 69 | eqtr4d 2659 |
. . . . 5
|
71 | 24, 70 | jca 554 |
. . . 4
|
72 | | simprr 796 |
. . . . . 6
|
73 | 2 | adantr 481 |
. . . . . . . 8
TopOn |
74 | 4 | adantr 481 |
. . . . . . . 8
TopOn |
75 | 12 | adantr 481 |
. . . . . . . 8
TopOn |
76 | | xkohmeo.k |
. . . . . . . . 9
𝑛Locally |
77 | 76 | adantr 481 |
. . . . . . . 8
𝑛Locally |
78 | | nllytop 21276 |
. . . . . . . . . . . . . 14
𝑛Locally |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . 13
|
80 | 9 | adantr 481 |
. . . . . . . . . . . . 13
|
81 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
82 | 81 | xkotopon 21403 |
. . . . . . . . . . . . 13
TopOn |
83 | 79, 80, 82 | syl2anc 693 |
. . . . . . . . . . . 12
TopOn |
84 | | simpr 477 |
. . . . . . . . . . . 12
|
85 | | cnf2 21053 |
. . . . . . . . . . . 12
TopOn TopOn
|
86 | 73, 83, 84, 85 | syl3anc 1326 |
. . . . . . . . . . 11
|
87 | 86 | feqmptd 6249 |
. . . . . . . . . 10
|
88 | 4 | ad2antrr 762 |
. . . . . . . . . . . . 13
TopOn |
89 | 12 | ad2antrr 762 |
. . . . . . . . . . . . 13
TopOn |
90 | 86 | ffvelrnda 6359 |
. . . . . . . . . . . . 13
|
91 | | cnf2 21053 |
. . . . . . . . . . . . 13
TopOn TopOn
|
92 | 88, 89, 90, 91 | syl3anc 1326 |
. . . . . . . . . . . 12
|
93 | 92 | feqmptd 6249 |
. . . . . . . . . . 11
|
94 | 93 | mpteq2dva 4744 |
. . . . . . . . . 10
|
95 | 87, 94 | eqtrd 2656 |
. . . . . . . . 9
|
96 | 95, 84 | eqeltrrd 2702 |
. . . . . . . 8
|
97 | 73, 74, 75, 77, 96 | cnmptk2 21489 |
. . . . . . 7
|
98 | 97 | adantrr 753 |
. . . . . 6
|
99 | 72, 98 | eqeltrd 2701 |
. . . . 5
|
100 | 95 | adantrr 753 |
. . . . . 6
|
101 | | nfv 1843 |
. . . . . . . . 9
|
102 | | nfmpt21 6722 |
. . . . . . . . . 10
|
103 | 102 | nfeq2 2780 |
. . . . . . . . 9
|
104 | 101, 103 | nfan 1828 |
. . . . . . . 8
|
105 | 27, 104 | nfan 1828 |
. . . . . . 7
|
106 | | nfv 1843 |
. . . . . . . . . . . 12
|
107 | | nfmpt22 6723 |
. . . . . . . . . . . . 13
|
108 | 107 | nfeq2 2780 |
. . . . . . . . . . . 12
|
109 | 106, 108 | nfan 1828 |
. . . . . . . . . . 11
|
110 | 33, 109 | nfan 1828 |
. . . . . . . . . 10
|
111 | 110, 41 | nfan 1828 |
. . . . . . . . 9
|
112 | 72 | oveqd 6667 |
. . . . . . . . . . 11
|
113 | | fvex 6201 |
. . . . . . . . . . . 12
|
114 | | eqid 2622 |
. . . . . . . . . . . . 13
|
115 | 114 | ovmpt4g 6783 |
. . . . . . . . . . . 12
|
116 | 113, 115 | mp3an3 1413 |
. . . . . . . . . . 11
|
117 | 112, 116 | sylan9eq 2676 |
. . . . . . . . . 10
|
118 | 117 | expr 643 |
. . . . . . . . 9
|
119 | 111, 118 | ralrimi 2957 |
. . . . . . . 8
|
120 | | mpteq12 4736 |
. . . . . . . 8
|
121 | 64, 119, 120 | sylancr 695 |
. . . . . . 7
|
122 | 105, 121 | mpteq2da 4743 |
. . . . . 6
|
123 | 100, 122 | eqtr4d 2659 |
. . . . 5
|
124 | 99, 123 | jca 554 |
. . . 4
|
125 | 71, 124 | impbida 877 |
. . 3
|
126 | 125 | opabbidv 4716 |
. 2
|
127 | | xkohmeo.f |
. . . . 5
|
128 | | df-mpt 4730 |
. . . . 5
|
129 | 127, 128 | eqtri 2644 |
. . . 4
|
130 | 129 | cnveqi 5297 |
. . 3
|
131 | | cnvopab 5533 |
. . 3
|
132 | 130, 131 | eqtri 2644 |
. 2
|
133 | | df-mpt 4730 |
. 2
|
134 | 126, 132,
133 | 3eqtr4g 2681 |
1
|