Step | Hyp | Ref
| Expression |
1 | | sconnpconn 31209 |
. . 3
SConn PConn |
2 | | sconnpconn 31209 |
. . 3
SConn PConn |
3 | | txpconn 31214 |
. . 3
PConn
PConn
PConn |
4 | 1, 2, 3 | syl2an 494 |
. 2
SConn
SConn
PConn |
5 | | simpll 790 |
. . . . . . . . 9
SConn SConn
SConn |
6 | | simprl 794 |
. . . . . . . . . 10
SConn SConn
|
7 | | sconntop 31210 |
. . . . . . . . . . . . 13
SConn |
8 | 7 | ad2antrr 762 |
. . . . . . . . . . . 12
SConn SConn
|
9 | | eqid 2622 |
. . . . . . . . . . . . 13
|
10 | 9 | toptopon 20722 |
. . . . . . . . . . . 12
TopOn |
11 | 8, 10 | sylib 208 |
. . . . . . . . . . 11
SConn SConn
TopOn |
12 | | sconntop 31210 |
. . . . . . . . . . . . 13
SConn |
13 | 12 | ad2antlr 763 |
. . . . . . . . . . . 12
SConn SConn
|
14 | | eqid 2622 |
. . . . . . . . . . . . 13
|
15 | 14 | toptopon 20722 |
. . . . . . . . . . . 12
TopOn |
16 | 13, 15 | sylib 208 |
. . . . . . . . . . 11
SConn SConn
TopOn |
17 | | tx1cn 21412 |
. . . . . . . . . . 11
TopOn TopOn
|
18 | 11, 16, 17 | syl2anc 693 |
. . . . . . . . . 10
SConn SConn
|
19 | | cnco 21070 |
. . . . . . . . . 10
|
20 | 6, 18, 19 | syl2anc 693 |
. . . . . . . . 9
SConn SConn
|
21 | | simprr 796 |
. . . . . . . . . . 11
SConn SConn
|
22 | 21 | fveq2d 6195 |
. . . . . . . . . 10
SConn SConn
|
23 | | iitopon 22682 |
. . . . . . . . . . . . 13
TopOn |
24 | 23 | a1i 11 |
. . . . . . . . . . . 12
SConn SConn
TopOn |
25 | | txtopon 21394 |
. . . . . . . . . . . . 13
TopOn TopOn
TopOn |
26 | 11, 16, 25 | syl2anc 693 |
. . . . . . . . . . . 12
SConn SConn
TopOn |
27 | | cnf2 21053 |
. . . . . . . . . . . 12
TopOn TopOn
|
28 | 24, 26, 6, 27 | syl3anc 1326 |
. . . . . . . . . . 11
SConn SConn
|
29 | | 0elunit 12290 |
. . . . . . . . . . 11
|
30 | | fvco3 6275 |
. . . . . . . . . . 11
|
31 | 28, 29, 30 | sylancl 694 |
. . . . . . . . . 10
SConn SConn
|
32 | | 1elunit 12291 |
. . . . . . . . . . 11
|
33 | | fvco3 6275 |
. . . . . . . . . . 11
|
34 | 28, 32, 33 | sylancl 694 |
. . . . . . . . . 10
SConn SConn
|
35 | 22, 31, 34 | 3eqtr4d 2666 |
. . . . . . . . 9
SConn SConn
|
36 | | sconnpht 31211 |
. . . . . . . . 9
SConn
|
37 | 5, 20, 35, 36 | syl3anc 1326 |
. . . . . . . 8
SConn SConn
|
38 | | isphtpc 22793 |
. . . . . . . 8
|
39 | 37, 38 | sylib 208 |
. . . . . . 7
SConn SConn
|
40 | 39 | simp3d 1075 |
. . . . . 6
SConn SConn
|
41 | | n0 3931 |
. . . . . 6
|
42 | 40, 41 | sylib 208 |
. . . . 5
SConn SConn
|
43 | | simplr 792 |
. . . . . . . . 9
SConn SConn
SConn |
44 | | tx2cn 21413 |
. . . . . . . . . . 11
TopOn TopOn
|
45 | 11, 16, 44 | syl2anc 693 |
. . . . . . . . . 10
SConn SConn
|
46 | | cnco 21070 |
. . . . . . . . . 10
|
47 | 6, 45, 46 | syl2anc 693 |
. . . . . . . . 9
SConn SConn
|
48 | 21 | fveq2d 6195 |
. . . . . . . . . 10
SConn SConn
|
49 | | fvco3 6275 |
. . . . . . . . . . 11
|
50 | 28, 29, 49 | sylancl 694 |
. . . . . . . . . 10
SConn SConn
|
51 | | fvco3 6275 |
. . . . . . . . . . 11
|
52 | 28, 32, 51 | sylancl 694 |
. . . . . . . . . 10
SConn SConn
|
53 | 48, 50, 52 | 3eqtr4d 2666 |
. . . . . . . . 9
SConn SConn
|
54 | | sconnpht 31211 |
. . . . . . . . 9
SConn
|
55 | 43, 47, 53, 54 | syl3anc 1326 |
. . . . . . . 8
SConn SConn
|
56 | | isphtpc 22793 |
. . . . . . . 8
|
57 | 55, 56 | sylib 208 |
. . . . . . 7
SConn SConn
|
58 | 57 | simp3d 1075 |
. . . . . 6
SConn SConn
|
59 | | n0 3931 |
. . . . . 6
|
60 | 58, 59 | sylib 208 |
. . . . 5
SConn SConn
|
61 | | eeanv 2182 |
. . . . . 6
|
62 | 8 | adantr 481 |
. . . . . . . . 9
SConn
SConn
|
63 | 13 | adantr 481 |
. . . . . . . . 9
SConn
SConn
|
64 | 6 | adantr 481 |
. . . . . . . . 9
SConn
SConn
|
65 | | eqid 2622 |
. . . . . . . . 9
|
66 | | eqid 2622 |
. . . . . . . . 9
|
67 | | simprl 794 |
. . . . . . . . 9
SConn
SConn
|
68 | | simprr 796 |
. . . . . . . . 9
SConn
SConn
|
69 | 62, 63, 64, 65, 66, 67, 68 | txsconnlem 31222 |
. . . . . . . 8
SConn
SConn
|
70 | 69 | ex 450 |
. . . . . . 7
SConn SConn
|
71 | 70 | exlimdvv 1862 |
. . . . . 6
SConn SConn
|
72 | 61, 71 | syl5bir 233 |
. . . . 5
SConn SConn
|
73 | 42, 60, 72 | mp2and 715 |
. . . 4
SConn SConn
|
74 | 73 | expr 643 |
. . 3
SConn SConn
|
75 | 74 | ralrimiva 2966 |
. 2
SConn
SConn
|
76 | | issconn 31208 |
. 2
SConn PConn
|
77 | 4, 75, 76 | sylanbrc 698 |
1
SConn
SConn
SConn |