Step | Hyp | Ref
| Expression |
1 | | txdis1cn.f |
. . 3
|
2 | | txdis1cn.j |
. . . . . . 7
TopOn |
3 | 2 | adantr 274 |
. . . . . 6
TopOn |
4 | | txdis1cn.k |
. . . . . . . 8
|
5 | | toptopon2 12186 |
. . . . . . . 8
TopOn |
6 | 4, 5 | sylib 121 |
. . . . . . 7
TopOn |
7 | 6 | adantr 274 |
. . . . . 6
TopOn |
8 | | txdis1cn.1 |
. . . . . 6
|
9 | | cnf2 12374 |
. . . . . 6
TopOn TopOn |
10 | 3, 7, 8, 9 | syl3anc 1216 |
. . . . 5
|
11 | | eqid 2139 |
. . . . . 6
|
12 | 11 | fmpt 5570 |
. . . . 5
|
13 | 10, 12 | sylibr 133 |
. . . 4
|
14 | 13 | ralrimiva 2505 |
. . 3
|
15 | | ffnov 5875 |
. . 3
|
16 | 1, 14, 15 | sylanbrc 413 |
. 2
|
17 | | cnvimass 4902 |
. . . . . . . 8
|
18 | 1 | adantr 274 |
. . . . . . . . 9
|
19 | | fndm 5222 |
. . . . . . . . 9
|
20 | 18, 19 | syl 14 |
. . . . . . . 8
|
21 | 17, 20 | sseqtrid 3147 |
. . . . . . 7
|
22 | | relxp 4648 |
. . . . . . 7
|
23 | | relss 4626 |
. . . . . . 7
|
24 | 21, 22, 23 | mpisyl 1422 |
. . . . . 6
|
25 | | elpreima 5539 |
. . . . . . . 8
|
26 | 18, 25 | syl 14 |
. . . . . . 7
|
27 | | opelxp 4569 |
. . . . . . . . 9
|
28 | | df-ov 5777 |
. . . . . . . . . . 11
|
29 | 28 | eqcomi 2143 |
. . . . . . . . . 10
|
30 | 29 | eleq1i 2205 |
. . . . . . . . 9
|
31 | 27, 30 | anbi12i 455 |
. . . . . . . 8
|
32 | | simprll 526 |
. . . . . . . . . . . 12
|
33 | | snelpwi 4134 |
. . . . . . . . . . . 12
|
34 | 32, 33 | syl 14 |
. . . . . . . . . . 11
|
35 | 11 | mptpreima 5032 |
. . . . . . . . . . . 12
|
36 | 8 | adantrr 470 |
. . . . . . . . . . . . . 14
|
37 | 36 | ad2ant2r 500 |
. . . . . . . . . . . . 13
|
38 | | simplr 519 |
. . . . . . . . . . . . 13
|
39 | | cnima 12389 |
. . . . . . . . . . . . 13
|
40 | 37, 38, 39 | syl2anc 408 |
. . . . . . . . . . . 12
|
41 | 35, 40 | eqeltrrid 2227 |
. . . . . . . . . . 11
|
42 | | simprlr 527 |
. . . . . . . . . . . 12
|
43 | | simprr 521 |
. . . . . . . . . . . 12
|
44 | | vsnid 3557 |
. . . . . . . . . . . . . 14
|
45 | | opelxp 4569 |
. . . . . . . . . . . . . 14
|
46 | 44, 45 | mpbiran 924 |
. . . . . . . . . . . . 13
|
47 | | oveq2 5782 |
. . . . . . . . . . . . . . 15
|
48 | 47 | eleq1d 2208 |
. . . . . . . . . . . . . 14
|
49 | 48 | elrab 2840 |
. . . . . . . . . . . . 13
|
50 | 46, 49 | bitri 183 |
. . . . . . . . . . . 12
|
51 | 42, 43, 50 | sylanbrc 413 |
. . . . . . . . . . 11
|
52 | | relxp 4648 |
. . . . . . . . . . . . 13
|
53 | 52 | a1i 9 |
. . . . . . . . . . . 12
|
54 | | opelxp 4569 |
. . . . . . . . . . . . 13
|
55 | 32 | snssd 3665 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55 | sselda 3097 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | adantrr 470 |
. . . . . . . . . . . . . . . 16
|
58 | | elrabi 2837 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | ad2antll 482 |
. . . . . . . . . . . . . . . 16
|
60 | 57, 59 | opelxpd 4572 |
. . . . . . . . . . . . . . 15
|
61 | | df-ov 5777 |
. . . . . . . . . . . . . . . . 17
|
62 | | elsni 3545 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 62 | ad2antrl 481 |
. . . . . . . . . . . . . . . . . 18
|
64 | 63 | oveq1d 5789 |
. . . . . . . . . . . . . . . . 17
|
65 | 61, 64 | syl5eqr 2186 |
. . . . . . . . . . . . . . . 16
|
66 | | oveq2 5782 |
. . . . . . . . . . . . . . . . . . . 20
|
67 | 66 | eleq1d 2208 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 67 | elrab 2840 |
. . . . . . . . . . . . . . . . . 18
|
69 | 68 | simprbi 273 |
. . . . . . . . . . . . . . . . 17
|
70 | 69 | ad2antll 482 |
. . . . . . . . . . . . . . . 16
|
71 | 65, 70 | eqeltrd 2216 |
. . . . . . . . . . . . . . 15
|
72 | | elpreima 5539 |
. . . . . . . . . . . . . . . . 17
|
73 | 1, 72 | syl 14 |
. . . . . . . . . . . . . . . 16
|
74 | 73 | ad3antrrr 483 |
. . . . . . . . . . . . . . 15
|
75 | 60, 71, 74 | mpbir2and 928 |
. . . . . . . . . . . . . 14
|
76 | 75 | ex 114 |
. . . . . . . . . . . . 13
|
77 | 54, 76 | syl5bi 151 |
. . . . . . . . . . . 12
|
78 | 53, 77 | relssdv 4631 |
. . . . . . . . . . 11
|
79 | | xpeq1 4553 |
. . . . . . . . . . . . . 14
|
80 | 79 | eleq2d 2209 |
. . . . . . . . . . . . 13
|
81 | 79 | sseq1d 3126 |
. . . . . . . . . . . . 13
|
82 | 80, 81 | anbi12d 464 |
. . . . . . . . . . . 12
|
83 | | xpeq2 4554 |
. . . . . . . . . . . . . 14
|
84 | 83 | eleq2d 2209 |
. . . . . . . . . . . . 13
|
85 | 83 | sseq1d 3126 |
. . . . . . . . . . . . 13
|
86 | 84, 85 | anbi12d 464 |
. . . . . . . . . . . 12
|
87 | 82, 86 | rspc2ev 2804 |
. . . . . . . . . . 11
|
88 | 34, 41, 51, 78, 87 | syl112anc 1220 |
. . . . . . . . . 10
|
89 | | vex 2689 |
. . . . . . . . . . . 12
|
90 | | vex 2689 |
. . . . . . . . . . . 12
|
91 | 89, 90 | opex 4151 |
. . . . . . . . . . 11
|
92 | | eleq1 2202 |
. . . . . . . . . . . . 13
|
93 | 92 | anbi1d 460 |
. . . . . . . . . . . 12
|
94 | 93 | 2rexbidv 2460 |
. . . . . . . . . . 11
|
95 | 91, 94 | elab 2828 |
. . . . . . . . . 10
|
96 | 88, 95 | sylibr 133 |
. . . . . . . . 9
|
97 | 96 | ex 114 |
. . . . . . . 8
|
98 | 31, 97 | syl5bi 151 |
. . . . . . 7
|
99 | 26, 98 | sylbid 149 |
. . . . . 6
|
100 | 24, 99 | relssdv 4631 |
. . . . 5
|
101 | | ssabral 3168 |
. . . . 5
|
102 | 100, 101 | sylib 121 |
. . . 4
|
103 | | txdis1cn.x |
. . . . . . 7
|
104 | | distopon 12256 |
. . . . . . 7
TopOn |
105 | 103, 104 | syl 14 |
. . . . . 6
TopOn |
106 | 105 | adantr 274 |
. . . . 5
TopOn |
107 | 2 | adantr 274 |
. . . . 5
TopOn |
108 | | eltx 12428 |
. . . . 5
TopOn TopOn
|
109 | 106, 107,
108 | syl2anc 408 |
. . . 4
|
110 | 102, 109 | mpbird 166 |
. . 3
|
111 | 110 | ralrimiva 2505 |
. 2
|
112 | | txtopon 12431 |
. . . 4
TopOn TopOn
TopOn |
113 | 105, 2, 112 | syl2anc 408 |
. . 3
TopOn |
114 | | iscn 12366 |
. . 3
TopOn TopOn
|
115 | 113, 6, 114 | syl2anc 408 |
. 2
|
116 | 16, 111, 115 | mpbir2and 928 |
1
|