Step | Hyp | Ref
| Expression |
1 | | conntop 21220 |
. . 3
Conn |
2 | | conntop 21220 |
. . 3
Conn |
3 | | txtop 21372 |
. . 3
|
4 | 1, 2, 3 | syl2an 494 |
. 2
Conn Conn
|
5 | | neq0 3930 |
. . . . . . 7
|
6 | | inss1 3833 |
. . . . . . . . . . . 12
|
7 | | simplr 792 |
. . . . . . . . . . . 12
Conn
Conn
|
8 | 6, 7 | sseldi 3601 |
. . . . . . . . . . 11
Conn
Conn
|
9 | | elssuni 4467 |
. . . . . . . . . . 11
|
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
Conn
Conn
|
11 | | simprr 796 |
. . . . . . . . . . . . . . 15
Conn
Conn
|
12 | | simplll 798 |
. . . . . . . . . . . . . . . . 17
Conn
Conn
Conn |
13 | 12, 1 | syl 17 |
. . . . . . . . . . . . . . . 16
Conn
Conn
|
14 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
Conn
Conn
Conn |
15 | 14, 2 | syl 17 |
. . . . . . . . . . . . . . . 16
Conn
Conn
|
16 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
17 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
18 | 16, 17 | txuni 21395 |
. . . . . . . . . . . . . . . 16
|
19 | 13, 15, 18 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Conn
Conn
|
20 | 11, 19 | eleqtrrd 2704 |
. . . . . . . . . . . . . 14
Conn
Conn
|
21 | | 1st2nd2 7205 |
. . . . . . . . . . . . . 14
|
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
Conn
Conn
|
23 | | xp2nd 7199 |
. . . . . . . . . . . . . . . 16
|
24 | 20, 23 | syl 17 |
. . . . . . . . . . . . . . 15
Conn
Conn
|
25 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
|
26 | 25 | mptpreima 5628 |
. . . . . . . . . . . . . . . . 17
|
27 | 17 | toptopon 20722 |
. . . . . . . . . . . . . . . . . . . 20
TopOn |
28 | 15, 27 | sylib 208 |
. . . . . . . . . . . . . . . . . . 19
Conn
Conn
TopOn |
29 | 16 | toptopon 20722 |
. . . . . . . . . . . . . . . . . . . . 21
TopOn |
30 | 13, 29 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
Conn
Conn
TopOn |
31 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 20, 31 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
Conn
Conn
|
33 | 28, 30, 32 | cnmptc 21465 |
. . . . . . . . . . . . . . . . . . 19
Conn
Conn
|
34 | 28 | cnmptid 21464 |
. . . . . . . . . . . . . . . . . . 19
Conn
Conn
|
35 | 28, 33, 34 | cnmpt1t 21468 |
. . . . . . . . . . . . . . . . . 18
Conn
Conn
|
36 | | simplr 792 |
. . . . . . . . . . . . . . . . . . 19
Conn
Conn
|
37 | 6, 36 | sseldi 3601 |
. . . . . . . . . . . . . . . . . 18
Conn
Conn
|
38 | | cnima 21069 |
. . . . . . . . . . . . . . . . . 18
|
39 | 35, 37, 38 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
Conn
Conn
|
40 | 26, 39 | syl5eqelr 2706 |
. . . . . . . . . . . . . . . 16
Conn
Conn
|
41 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . 21
Conn
Conn
|
42 | | elunii 4441 |
. . . . . . . . . . . . . . . . . . . . 21
|
43 | 41, 37, 42 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . 20
Conn
Conn
|
44 | 43, 19 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . 19
Conn
Conn
|
45 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . 19
|
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Conn
Conn
|
47 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
48 | 47 | mptpreima 5628 |
. . . . . . . . . . . . . . . . . . . . . 22
|
49 | 30 | cnmptid 21464 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Conn
Conn
|
50 | 30, 28, 46 | cnmptc 21465 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Conn
Conn
|
51 | 30, 49, 50 | cnmpt1t 21468 |
. . . . . . . . . . . . . . . . . . . . . . 23
Conn
Conn
|
52 | | cnima 21069 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
53 | 51, 37, 52 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
Conn
Conn
|
54 | 48, 53 | syl5eqelr 2706 |
. . . . . . . . . . . . . . . . . . . . 21
Conn
Conn
|
55 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
56 | 44, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
Conn
Conn
|
57 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
58 | 44, 57 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Conn
Conn
|
59 | 58, 41 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . . . . . . . . 23
Conn
Conn
|
60 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
61 | 60 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
62 | 61 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
63 | 56, 59, 62 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
Conn
Conn
|
64 | | rabn0 3958 |
. . . . . . . . . . . . . . . . . . . . . 22
|
65 | 63, 64 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . 21
Conn
Conn
|
66 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
67 | 66, 36 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . 23
Conn
Conn
|
68 | | cnclima 21072 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
69 | 51, 67, 68 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
Conn
Conn
|
70 | 48, 69 | syl5eqelr 2706 |
. . . . . . . . . . . . . . . . . . . . 21
Conn
Conn
|
71 | 16, 12, 54, 65, 70 | connclo 21218 |
. . . . . . . . . . . . . . . . . . . 20
Conn
Conn
|
72 | 32, 71 | eleqtrrd 2704 |
. . . . . . . . . . . . . . . . . . 19
Conn
Conn
|
73 | | opeq1 4402 |
. . . . . . . . . . . . . . . . . . . . . 22
|
74 | 73 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . 21
|
75 | 74 | elrab 3363 |
. . . . . . . . . . . . . . . . . . . 20
|
76 | 75 | simprbi 480 |
. . . . . . . . . . . . . . . . . . 19
|
77 | 72, 76 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Conn
Conn
|
78 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 78 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
80 | 79 | rspcev 3309 |
. . . . . . . . . . . . . . . . . 18
|
81 | 46, 77, 80 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
Conn
Conn
|
82 | | rabn0 3958 |
. . . . . . . . . . . . . . . . 17
|
83 | 81, 82 | sylibr 224 |
. . . . . . . . . . . . . . . 16
Conn
Conn
|
84 | | cnclima 21072 |
. . . . . . . . . . . . . . . . . 18
|
85 | 35, 67, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
Conn
Conn
|
86 | 26, 85 | syl5eqelr 2706 |
. . . . . . . . . . . . . . . 16
Conn
Conn
|
87 | 17, 14, 40, 83, 86 | connclo 21218 |
. . . . . . . . . . . . . . 15
Conn
Conn
|
88 | 24, 87 | eleqtrrd 2704 |
. . . . . . . . . . . . . 14
Conn
Conn
|
89 | | opeq2 4403 |
. . . . . . . . . . . . . . . . 17
|
90 | 89 | eleq1d 2686 |
. . . . . . . . . . . . . . . 16
|
91 | 90 | elrab 3363 |
. . . . . . . . . . . . . . 15
|
92 | 91 | simprbi 480 |
. . . . . . . . . . . . . 14
|
93 | 88, 92 | syl 17 |
. . . . . . . . . . . . 13
Conn
Conn
|
94 | 22, 93 | eqeltrd 2701 |
. . . . . . . . . . . 12
Conn
Conn
|
95 | 94 | expr 643 |
. . . . . . . . . . 11
Conn
Conn
|
96 | 95 | ssrdv 3609 |
. . . . . . . . . 10
Conn
Conn
|
97 | 10, 96 | eqssd 3620 |
. . . . . . . . 9
Conn
Conn
|
98 | 97 | ex 450 |
. . . . . . . 8
Conn
Conn
|
99 | 98 | exlimdv 1861 |
. . . . . . 7
Conn
Conn
|
100 | 5, 99 | syl5bi 232 |
. . . . . 6
Conn
Conn
|
101 | 100 | orrd 393 |
. . . . 5
Conn
Conn
|
102 | 101 | ex 450 |
. . . 4
Conn Conn
|
103 | | vex 3203 |
. . . . 5
|
104 | 103 | elpr 4198 |
. . . 4
|
105 | 102, 104 | syl6ibr 242 |
. . 3
Conn Conn
|
106 | 105 | ssrdv 3609 |
. 2
Conn Conn
|
107 | | eqid 2622 |
. . 3
|
108 | 107 | isconn2 21217 |
. 2
Conn
|
109 | 4, 106, 108 | sylanbrc 698 |
1
Conn Conn
Conn |