Step | Hyp | Ref
| Expression |
1 | | conncn.f |
. . . 4
β’ (π β πΉ β (π½ Cn πΎ)) |
2 | | conncn.x |
. . . . 5
β’ π = βͺ
π½ |
3 | | eqid 2733 |
. . . . 5
β’ βͺ πΎ =
βͺ πΎ |
4 | 2, 3 | cnf 22620 |
. . . 4
β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆβͺ πΎ) |
5 | 1, 4 | syl 17 |
. . 3
β’ (π β πΉ:πβΆβͺ πΎ) |
6 | 5 | ffnd 6673 |
. 2
β’ (π β πΉ Fn π) |
7 | 5 | frnd 6680 |
. . 3
β’ (π β ran πΉ β βͺ πΎ) |
8 | | conncn.j |
. . . 4
β’ (π β π½ β Conn) |
9 | | dffn4 6766 |
. . . . . 6
β’ (πΉ Fn π β πΉ:πβontoβran πΉ) |
10 | 6, 9 | sylib 217 |
. . . . 5
β’ (π β πΉ:πβontoβran πΉ) |
11 | | cntop2 22615 |
. . . . . . . 8
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
12 | 1, 11 | syl 17 |
. . . . . . 7
β’ (π β πΎ β Top) |
13 | 3 | restuni 22536 |
. . . . . . 7
β’ ((πΎ β Top β§ ran πΉ β βͺ πΎ)
β ran πΉ = βͺ (πΎ
βΎt ran πΉ)) |
14 | 12, 7, 13 | syl2anc 585 |
. . . . . 6
β’ (π β ran πΉ = βͺ (πΎ βΎt ran πΉ)) |
15 | | foeq3 6758 |
. . . . . 6
β’ (ran
πΉ = βͺ (πΎ
βΎt ran πΉ)
β (πΉ:πβontoβran πΉ β πΉ:πβontoββͺ (πΎ βΎt ran πΉ))) |
16 | 14, 15 | syl 17 |
. . . . 5
β’ (π β (πΉ:πβontoβran πΉ β πΉ:πβontoββͺ (πΎ βΎt ran πΉ))) |
17 | 10, 16 | mpbid 231 |
. . . 4
β’ (π β πΉ:πβontoββͺ (πΎ βΎt ran πΉ)) |
18 | | toptopon2 22290 |
. . . . . . 7
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
19 | 12, 18 | sylib 217 |
. . . . . 6
β’ (π β πΎ β (TopOnββͺ πΎ)) |
20 | | ssidd 3971 |
. . . . . 6
β’ (π β ran πΉ β ran πΉ) |
21 | | cnrest2 22660 |
. . . . . 6
β’ ((πΎ β (TopOnββͺ πΎ)
β§ ran πΉ β ran
πΉ β§ ran πΉ β βͺ πΎ)
β (πΉ β (π½ Cn πΎ) β πΉ β (π½ Cn (πΎ βΎt ran πΉ)))) |
22 | 19, 20, 7, 21 | syl3anc 1372 |
. . . . 5
β’ (π β (πΉ β (π½ Cn πΎ) β πΉ β (π½ Cn (πΎ βΎt ran πΉ)))) |
23 | 1, 22 | mpbid 231 |
. . . 4
β’ (π β πΉ β (π½ Cn (πΎ βΎt ran πΉ))) |
24 | | eqid 2733 |
. . . . 5
β’ βͺ (πΎ
βΎt ran πΉ)
= βͺ (πΎ βΎt ran πΉ) |
25 | 24 | cnconn 22796 |
. . . 4
β’ ((π½ β Conn β§ πΉ:πβontoββͺ (πΎ βΎt ran πΉ) β§ πΉ β (π½ Cn (πΎ βΎt ran πΉ))) β (πΎ βΎt ran πΉ) β Conn) |
26 | 8, 17, 23, 25 | syl3anc 1372 |
. . 3
β’ (π β (πΎ βΎt ran πΉ) β Conn) |
27 | | conncn.u |
. . 3
β’ (π β π β πΎ) |
28 | | conncn.1 |
. . . 4
β’ (π β (πΉβπ΄) β π) |
29 | | conncn.a |
. . . . 5
β’ (π β π΄ β π) |
30 | | fnfvelrn 7035 |
. . . . 5
β’ ((πΉ Fn π β§ π΄ β π) β (πΉβπ΄) β ran πΉ) |
31 | 6, 29, 30 | syl2anc 585 |
. . . 4
β’ (π β (πΉβπ΄) β ran πΉ) |
32 | | inelcm 4428 |
. . . 4
β’ (((πΉβπ΄) β π β§ (πΉβπ΄) β ran πΉ) β (π β© ran πΉ) β β
) |
33 | 28, 31, 32 | syl2anc 585 |
. . 3
β’ (π β (π β© ran πΉ) β β
) |
34 | | conncn.c |
. . 3
β’ (π β π β (ClsdβπΎ)) |
35 | 3, 7, 26, 27, 33, 34 | connsubclo 22798 |
. 2
β’ (π β ran πΉ β π) |
36 | | df-f 6504 |
. 2
β’ (πΉ:πβΆπ β (πΉ Fn π β§ ran πΉ β π)) |
37 | 6, 35, 36 | sylanbrc 584 |
1
β’ (π β πΉ:πβΆπ) |