Step | Hyp | Ref
| Expression |
1 | | n0 3931 |
. . 3
|
2 | | uniiun 4573 |
. . . . . . . . 9
|
3 | | simpl1 1064 |
. . . . . . . . . . . 12
TopOn
↾t Conn
↾t Conn
TopOn |
4 | | toponmax 20730 |
. . . . . . . . . . . 12
TopOn
|
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
TopOn
↾t Conn
↾t Conn
|
6 | | simpl2l 1114 |
. . . . . . . . . . 11
TopOn
↾t Conn
↾t Conn
|
7 | 5, 6 | ssexd 4805 |
. . . . . . . . . 10
TopOn
↾t Conn
↾t Conn
|
8 | | simpl2r 1115 |
. . . . . . . . . . 11
TopOn
↾t Conn
↾t Conn
|
9 | 5, 8 | ssexd 4805 |
. . . . . . . . . 10
TopOn
↾t Conn
↾t Conn
|
10 | | uniprg 4450 |
. . . . . . . . . 10
|
11 | 7, 9, 10 | syl2anc 693 |
. . . . . . . . 9
TopOn
↾t Conn
↾t Conn
|
12 | 2, 11 | syl5eqr 2670 |
. . . . . . . 8
TopOn
↾t Conn
↾t Conn
|
13 | 12 | oveq2d 6666 |
. . . . . . 7
TopOn
↾t Conn
↾t Conn
↾t
↾t |
14 | | vex 3203 |
. . . . . . . . . 10
|
15 | 14 | elpr 4198 |
. . . . . . . . 9
|
16 | | simpl2 1065 |
. . . . . . . . . 10
TopOn
↾t Conn
↾t Conn
|
17 | | sseq1 3626 |
. . . . . . . . . . . 12
|
18 | 17 | biimprd 238 |
. . . . . . . . . . 11
|
19 | | sseq1 3626 |
. . . . . . . . . . . 12
|
20 | 19 | biimprd 238 |
. . . . . . . . . . 11
|
21 | 18, 20 | jaoa 532 |
. . . . . . . . . 10
|
22 | 16, 21 | mpan9 486 |
. . . . . . . . 9
TopOn
↾t Conn
↾t Conn
|
23 | 15, 22 | sylan2b 492 |
. . . . . . . 8
TopOn
↾t Conn
↾t Conn
|
24 | | simpl3 1066 |
. . . . . . . . . . 11
TopOn
↾t Conn
↾t Conn
|
25 | | elin 3796 |
. . . . . . . . . . 11
|
26 | 24, 25 | sylib 208 |
. . . . . . . . . 10
TopOn
↾t Conn
↾t Conn
|
27 | | eleq2 2690 |
. . . . . . . . . . . 12
|
28 | 27 | biimprd 238 |
. . . . . . . . . . 11
|
29 | | eleq2 2690 |
. . . . . . . . . . . 12
|
30 | 29 | biimprd 238 |
. . . . . . . . . . 11
|
31 | 28, 30 | jaoa 532 |
. . . . . . . . . 10
|
32 | 26, 31 | mpan9 486 |
. . . . . . . . 9
TopOn
↾t Conn
↾t Conn
|
33 | 15, 32 | sylan2b 492 |
. . . . . . . 8
TopOn
↾t Conn
↾t Conn
|
34 | | simpr 477 |
. . . . . . . . . 10
TopOn
↾t Conn
↾t Conn
↾t Conn
↾t Conn |
35 | | oveq2 6658 |
. . . . . . . . . . . . 13
↾t ↾t |
36 | 35 | eleq1d 2686 |
. . . . . . . . . . . 12
↾t Conn ↾t Conn |
37 | 36 | biimprd 238 |
. . . . . . . . . . 11
↾t Conn ↾t Conn |
38 | | oveq2 6658 |
. . . . . . . . . . . . 13
↾t ↾t |
39 | 38 | eleq1d 2686 |
. . . . . . . . . . . 12
↾t Conn ↾t Conn |
40 | 39 | biimprd 238 |
. . . . . . . . . . 11
↾t Conn ↾t Conn |
41 | 37, 40 | jaoa 532 |
. . . . . . . . . 10
↾t Conn ↾t Conn
↾t Conn |
42 | 34, 41 | mpan9 486 |
. . . . . . . . 9
TopOn
↾t Conn
↾t Conn
↾t Conn |
43 | 15, 42 | sylan2b 492 |
. . . . . . . 8
TopOn
↾t Conn
↾t Conn
↾t
Conn |
44 | 3, 23, 33, 43 | iunconn 21231 |
. . . . . . 7
TopOn
↾t Conn
↾t Conn
↾t Conn |
45 | 13, 44 | eqeltrrd 2702 |
. . . . . 6
TopOn
↾t Conn
↾t Conn
↾t
Conn |
46 | 45 | ex 450 |
. . . . 5
TopOn ↾t Conn
↾t
Conn ↾t Conn |
47 | 46 | 3expia 1267 |
. . . 4
TopOn ↾t Conn
↾t Conn
↾t Conn |
48 | 47 | exlimdv 1861 |
. . 3
TopOn
↾t Conn
↾t Conn
↾t Conn |
49 | 1, 48 | syl5bi 232 |
. 2
TopOn ↾t Conn
↾t
Conn ↾t Conn |
50 | 49 | 3impia 1261 |
1
TopOn
↾t Conn
↾t Conn
↾t Conn |