Step | Hyp | Ref
| Expression |
1 | | simpll3 1102 |
. . . . 5
TopOn
↾t Conn
↾t Conn |
2 | | simpll1 1100 |
. . . . . . 7
TopOn
↾t Conn
TopOn |
3 | | simpll2 1101 |
. . . . . . 7
TopOn
↾t Conn
|
4 | | simplrl 800 |
. . . . . . 7
TopOn
↾t Conn
|
5 | | simplrr 801 |
. . . . . . 7
TopOn
↾t Conn
|
6 | | simprl1 1106 |
. . . . . . . . 9
TopOn
↾t Conn
|
7 | | n0 3931 |
. . . . . . . . 9
|
8 | 6, 7 | sylib 208 |
. . . . . . . 8
TopOn
↾t Conn
|
9 | 2 | adantr 481 |
. . . . . . . . . 10
TopOn
↾t Conn
TopOn |
10 | | topontop 20718 |
. . . . . . . . . 10
TopOn
|
11 | 9, 10 | syl 17 |
. . . . . . . . 9
TopOn
↾t Conn
|
12 | 3 | adantr 481 |
. . . . . . . . . 10
TopOn
↾t Conn
|
13 | | toponuni 20719 |
. . . . . . . . . . 11
TopOn
|
14 | 9, 13 | syl 17 |
. . . . . . . . . 10
TopOn
↾t Conn
|
15 | 12, 14 | sseqtrd 3641 |
. . . . . . . . 9
TopOn
↾t Conn
|
16 | | inss2 3834 |
. . . . . . . . . 10
|
17 | | simpr 477 |
. . . . . . . . . 10
TopOn
↾t Conn
|
18 | 16, 17 | sseldi 3601 |
. . . . . . . . 9
TopOn
↾t Conn
|
19 | 4 | adantr 481 |
. . . . . . . . 9
TopOn
↾t Conn
|
20 | | inss1 3833 |
. . . . . . . . . 10
|
21 | 20, 17 | sseldi 3601 |
. . . . . . . . 9
TopOn
↾t Conn
|
22 | | eqid 2622 |
. . . . . . . . . 10
|
23 | 22 | clsndisj 20879 |
. . . . . . . . 9
|
24 | 11, 15, 18, 19, 21, 23 | syl32anc 1334 |
. . . . . . . 8
TopOn
↾t Conn
|
25 | 8, 24 | exlimddv 1863 |
. . . . . . 7
TopOn
↾t Conn
|
26 | | simprl2 1107 |
. . . . . . . . 9
TopOn
↾t Conn
|
27 | | n0 3931 |
. . . . . . . . 9
|
28 | 26, 27 | sylib 208 |
. . . . . . . 8
TopOn
↾t Conn
|
29 | 2 | adantr 481 |
. . . . . . . . . 10
TopOn
↾t Conn
TopOn |
30 | 29, 10 | syl 17 |
. . . . . . . . 9
TopOn
↾t Conn
|
31 | 3 | adantr 481 |
. . . . . . . . . 10
TopOn
↾t Conn
|
32 | 29, 13 | syl 17 |
. . . . . . . . . 10
TopOn
↾t Conn
|
33 | 31, 32 | sseqtrd 3641 |
. . . . . . . . 9
TopOn
↾t Conn
|
34 | | inss2 3834 |
. . . . . . . . . 10
|
35 | | simpr 477 |
. . . . . . . . . 10
TopOn
↾t Conn
|
36 | 34, 35 | sseldi 3601 |
. . . . . . . . 9
TopOn
↾t Conn
|
37 | 5 | adantr 481 |
. . . . . . . . 9
TopOn
↾t Conn
|
38 | | inss1 3833 |
. . . . . . . . . 10
|
39 | 38, 35 | sseldi 3601 |
. . . . . . . . 9
TopOn
↾t Conn
|
40 | 22 | clsndisj 20879 |
. . . . . . . . 9
|
41 | 30, 33, 36, 37, 39, 40 | syl32anc 1334 |
. . . . . . . 8
TopOn
↾t Conn
|
42 | 28, 41 | exlimddv 1863 |
. . . . . . 7
TopOn
↾t Conn
|
43 | | simprl3 1108 |
. . . . . . . . . 10
TopOn
↾t Conn
|
44 | 2, 10 | syl 17 |
. . . . . . . . . . . 12
TopOn
↾t Conn
|
45 | 2, 13 | syl 17 |
. . . . . . . . . . . . 13
TopOn
↾t Conn
|
46 | 3, 45 | sseqtrd 3641 |
. . . . . . . . . . . 12
TopOn
↾t Conn
|
47 | 22 | sscls 20860 |
. . . . . . . . . . . 12
|
48 | 44, 46, 47 | syl2anc 693 |
. . . . . . . . . . 11
TopOn
↾t Conn
|
49 | 48 | sscond 3747 |
. . . . . . . . . 10
TopOn
↾t Conn
|
50 | 43, 49 | sstrd 3613 |
. . . . . . . . 9
TopOn
↾t Conn
|
51 | | ssv 3625 |
. . . . . . . . . 10
|
52 | | ssdif 3745 |
. . . . . . . . . 10
|
53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
|
54 | 50, 53 | syl6ss 3615 |
. . . . . . . 8
TopOn
↾t Conn
|
55 | | disj2 4024 |
. . . . . . . 8
|
56 | 54, 55 | sylibr 224 |
. . . . . . 7
TopOn
↾t Conn
|
57 | | simprr 796 |
. . . . . . . 8
TopOn
↾t Conn
|
58 | 48, 57 | sstrd 3613 |
. . . . . . 7
TopOn
↾t Conn
|
59 | 2, 3, 4, 5, 25, 42, 56, 58 | nconnsubb 21226 |
. . . . . 6
TopOn
↾t Conn
↾t Conn |
60 | 59 | expr 643 |
. . . . 5
TopOn
↾t Conn
↾t Conn |
61 | 1, 60 | mt2d 131 |
. . . 4
TopOn
↾t Conn
|
62 | 61 | ex 450 |
. . 3
TopOn ↾t Conn
|
63 | 62 | ralrimivva 2971 |
. 2
TopOn ↾t Conn
|
64 | | simp1 1061 |
. . 3
TopOn ↾t Conn
TopOn |
65 | 13 | sseq2d 3633 |
. . . . . . 7
TopOn
|
66 | 65 | biimpa 501 |
. . . . . 6
TopOn |
67 | 22 | clsss3 20863 |
. . . . . . 7
|
68 | 10, 67 | sylan 488 |
. . . . . 6
TopOn |
69 | 66, 68 | syldan 487 |
. . . . 5
TopOn |
70 | 13 | adantr 481 |
. . . . 5
TopOn |
71 | 69, 70 | sseqtr4d 3642 |
. . . 4
TopOn |
72 | 71 | 3adant3 1081 |
. . 3
TopOn ↾t Conn |
73 | | connsub 21224 |
. . 3
TopOn
↾t Conn
|
74 | 64, 72, 73 | syl2anc 693 |
. 2
TopOn ↾t Conn ↾t Conn
|
75 | 63, 74 | mpbird 247 |
1
TopOn ↾t Conn
↾t Conn |