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 12564 |
. . . . . . . 8
TopOn |
6 | 4, 5 | sylib 121 |
. . . . . . 7
TopOn |
7 | 6 | adantr 274 |
. . . . . 6
TopOn |
8 | | txdis1cn.1 |
. . . . . 6
|
9 | | cnf2 12752 |
. . . . . 6
TopOn TopOn |
10 | 3, 7, 8, 9 | syl3anc 1227 |
. . . . 5
|
11 | | eqid 2164 |
. . . . . 6
|
12 | 11 | fmpt 5629 |
. . . . 5
|
13 | 10, 12 | sylibr 133 |
. . . 4
|
14 | 13 | ralrimiva 2537 |
. . 3
|
15 | | ffnov 5937 |
. . 3
|
16 | 1, 14, 15 | sylanbrc 414 |
. 2
|
17 | | cnvimass 4961 |
. . . . . . . 8
|
18 | 1 | adantr 274 |
. . . . . . . . 9
|
19 | | fndm 5281 |
. . . . . . . . 9
|
20 | 18, 19 | syl 14 |
. . . . . . . 8
|
21 | 17, 20 | sseqtrid 3187 |
. . . . . . 7
|
22 | | relxp 4707 |
. . . . . . 7
|
23 | | relss 4685 |
. . . . . . 7
|
24 | 21, 22, 23 | mpisyl 1433 |
. . . . . 6
|
25 | | elpreima 5598 |
. . . . . . . 8
|
26 | 18, 25 | syl 14 |
. . . . . . 7
|
27 | | opelxp 4628 |
. . . . . . . . 9
|
28 | | df-ov 5839 |
. . . . . . . . . . 11
|
29 | 28 | eqcomi 2168 |
. . . . . . . . . 10
|
30 | 29 | eleq1i 2230 |
. . . . . . . . 9
|
31 | 27, 30 | anbi12i 456 |
. . . . . . . 8
|
32 | | simprll 527 |
. . . . . . . . . . . 12
|
33 | | snelpwi 4184 |
. . . . . . . . . . . 12
|
34 | 32, 33 | syl 14 |
. . . . . . . . . . 11
|
35 | 11 | mptpreima 5091 |
. . . . . . . . . . . 12
|
36 | 8 | adantrr 471 |
. . . . . . . . . . . . . 14
|
37 | 36 | ad2ant2r 501 |
. . . . . . . . . . . . 13
|
38 | | simplr 520 |
. . . . . . . . . . . . 13
|
39 | | cnima 12767 |
. . . . . . . . . . . . 13
|
40 | 37, 38, 39 | syl2anc 409 |
. . . . . . . . . . . 12
|
41 | 35, 40 | eqeltrrid 2252 |
. . . . . . . . . . 11
|
42 | | simprlr 528 |
. . . . . . . . . . . 12
|
43 | | simprr 522 |
. . . . . . . . . . . 12
|
44 | | vsnid 3602 |
. . . . . . . . . . . . . 14
|
45 | | opelxp 4628 |
. . . . . . . . . . . . . 14
|
46 | 44, 45 | mpbiran 929 |
. . . . . . . . . . . . 13
|
47 | | oveq2 5844 |
. . . . . . . . . . . . . . 15
|
48 | 47 | eleq1d 2233 |
. . . . . . . . . . . . . 14
|
49 | 48 | elrab 2877 |
. . . . . . . . . . . . 13
|
50 | 46, 49 | bitri 183 |
. . . . . . . . . . . 12
|
51 | 42, 43, 50 | sylanbrc 414 |
. . . . . . . . . . 11
|
52 | | relxp 4707 |
. . . . . . . . . . . . 13
|
53 | 52 | a1i 9 |
. . . . . . . . . . . 12
|
54 | | opelxp 4628 |
. . . . . . . . . . . . 13
|
55 | 32 | snssd 3712 |
. . . . . . . . . . . . . . . . . 18
|
56 | 55 | sselda 3137 |
. . . . . . . . . . . . . . . . 17
|
57 | 56 | adantrr 471 |
. . . . . . . . . . . . . . . 16
|
58 | | elrabi 2874 |
. . . . . . . . . . . . . . . . 17
|
59 | 58 | ad2antll 483 |
. . . . . . . . . . . . . . . 16
|
60 | 57, 59 | opelxpd 4631 |
. . . . . . . . . . . . . . 15
|
61 | | df-ov 5839 |
. . . . . . . . . . . . . . . . 17
|
62 | | elsni 3588 |
. . . . . . . . . . . . . . . . . . 19
|
63 | 62 | ad2antrl 482 |
. . . . . . . . . . . . . . . . . 18
|
64 | 63 | oveq1d 5851 |
. . . . . . . . . . . . . . . . 17
|
65 | 61, 64 | eqtr3id 2211 |
. . . . . . . . . . . . . . . 16
|
66 | | oveq2 5844 |
. . . . . . . . . . . . . . . . . . . 20
|
67 | 66 | eleq1d 2233 |
. . . . . . . . . . . . . . . . . . 19
|
68 | 67 | elrab 2877 |
. . . . . . . . . . . . . . . . . 18
|
69 | 68 | simprbi 273 |
. . . . . . . . . . . . . . . . 17
|
70 | 69 | ad2antll 483 |
. . . . . . . . . . . . . . . 16
|
71 | 65, 70 | eqeltrd 2241 |
. . . . . . . . . . . . . . 15
|
72 | | elpreima 5598 |
. . . . . . . . . . . . . . . . 17
|
73 | 1, 72 | syl 14 |
. . . . . . . . . . . . . . . 16
|
74 | 73 | ad3antrrr 484 |
. . . . . . . . . . . . . . 15
|
75 | 60, 71, 74 | mpbir2and 933 |
. . . . . . . . . . . . . 14
|
76 | 75 | ex 114 |
. . . . . . . . . . . . 13
|
77 | 54, 76 | syl5bi 151 |
. . . . . . . . . . . 12
|
78 | 53, 77 | relssdv 4690 |
. . . . . . . . . . 11
|
79 | | xpeq1 4612 |
. . . . . . . . . . . . . 14
|
80 | 79 | eleq2d 2234 |
. . . . . . . . . . . . 13
|
81 | 79 | sseq1d 3166 |
. . . . . . . . . . . . 13
|
82 | 80, 81 | anbi12d 465 |
. . . . . . . . . . . 12
|
83 | | xpeq2 4613 |
. . . . . . . . . . . . . 14
|
84 | 83 | eleq2d 2234 |
. . . . . . . . . . . . 13
|
85 | 83 | sseq1d 3166 |
. . . . . . . . . . . . 13
|
86 | 84, 85 | anbi12d 465 |
. . . . . . . . . . . 12
|
87 | 82, 86 | rspc2ev 2840 |
. . . . . . . . . . 11
|
88 | 34, 41, 51, 78, 87 | syl112anc 1231 |
. . . . . . . . . 10
|
89 | | vex 2724 |
. . . . . . . . . . . 12
|
90 | | vex 2724 |
. . . . . . . . . . . 12
|
91 | 89, 90 | opex 4201 |
. . . . . . . . . . 11
|
92 | | eleq1 2227 |
. . . . . . . . . . . . 13
|
93 | 92 | anbi1d 461 |
. . . . . . . . . . . 12
|
94 | 93 | 2rexbidv 2489 |
. . . . . . . . . . 11
|
95 | 91, 94 | elab 2865 |
. . . . . . . . . 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 4690 |
. . . . 5
|
101 | | ssabral 3208 |
. . . . 5
|
102 | 100, 101 | sylib 121 |
. . . 4
|
103 | | txdis1cn.x |
. . . . . . 7
|
104 | | distopon 12634 |
. . . . . . 7
TopOn |
105 | 103, 104 | syl 14 |
. . . . . 6
TopOn |
106 | 105 | adantr 274 |
. . . . 5
TopOn |
107 | 2 | adantr 274 |
. . . . 5
TopOn |
108 | | eltx 12806 |
. . . . 5
TopOn TopOn
|
109 | 106, 107,
108 | syl2anc 409 |
. . . 4
|
110 | 102, 109 | mpbird 166 |
. . 3
|
111 | 110 | ralrimiva 2537 |
. 2
|
112 | | txtopon 12809 |
. . . 4
TopOn TopOn
TopOn |
113 | 105, 2, 112 | syl2anc 409 |
. . 3
TopOn |
114 | | iscn 12744 |
. . 3
TopOn TopOn
|
115 | 113, 6, 114 | syl2anc 409 |
. 2
|
116 | 16, 111, 115 | mpbir2and 933 |
1
|