Step | Hyp | Ref
| Expression |
1 | | connima.c |
. 2
β’ (π β (π½ βΎt π΄) β Conn) |
2 | | connima.f |
. . . . . 6
β’ (π β πΉ β (π½ Cn πΎ)) |
3 | | connima.x |
. . . . . . 7
β’ π = βͺ
π½ |
4 | | eqid 2733 |
. . . . . . 7
β’ βͺ πΎ =
βͺ πΎ |
5 | 3, 4 | cnf 22620 |
. . . . . 6
β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆβͺ πΎ) |
6 | 2, 5 | syl 17 |
. . . . 5
β’ (π β πΉ:πβΆβͺ πΎ) |
7 | 6 | ffund 6676 |
. . . 4
β’ (π β Fun πΉ) |
8 | | connima.a |
. . . . 5
β’ (π β π΄ β π) |
9 | 6 | fdmd 6683 |
. . . . 5
β’ (π β dom πΉ = π) |
10 | 8, 9 | sseqtrrd 3989 |
. . . 4
β’ (π β π΄ β dom πΉ) |
11 | | fores 6770 |
. . . 4
β’ ((Fun
πΉ β§ π΄ β dom πΉ) β (πΉ βΎ π΄):π΄βontoβ(πΉ β π΄)) |
12 | 7, 10, 11 | syl2anc 585 |
. . 3
β’ (π β (πΉ βΎ π΄):π΄βontoβ(πΉ β π΄)) |
13 | | cntop2 22615 |
. . . . . 6
β’ (πΉ β (π½ Cn πΎ) β πΎ β Top) |
14 | 2, 13 | syl 17 |
. . . . 5
β’ (π β πΎ β Top) |
15 | | imassrn 6028 |
. . . . . 6
β’ (πΉ β π΄) β ran πΉ |
16 | 6 | frnd 6680 |
. . . . . 6
β’ (π β ran πΉ β βͺ πΎ) |
17 | 15, 16 | sstrid 3959 |
. . . . 5
β’ (π β (πΉ β π΄) β βͺ πΎ) |
18 | 4 | restuni 22536 |
. . . . 5
β’ ((πΎ β Top β§ (πΉ β π΄) β βͺ πΎ) β (πΉ β π΄) = βͺ (πΎ βΎt (πΉ β π΄))) |
19 | 14, 17, 18 | syl2anc 585 |
. . . 4
β’ (π β (πΉ β π΄) = βͺ (πΎ βΎt (πΉ β π΄))) |
20 | | foeq3 6758 |
. . . 4
β’ ((πΉ β π΄) = βͺ (πΎ βΎt (πΉ β π΄)) β ((πΉ βΎ π΄):π΄βontoβ(πΉ β π΄) β (πΉ βΎ π΄):π΄βontoββͺ (πΎ βΎt (πΉ β π΄)))) |
21 | 19, 20 | syl 17 |
. . 3
β’ (π β ((πΉ βΎ π΄):π΄βontoβ(πΉ β π΄) β (πΉ βΎ π΄):π΄βontoββͺ (πΎ βΎt (πΉ β π΄)))) |
22 | 12, 21 | mpbid 231 |
. 2
β’ (π β (πΉ βΎ π΄):π΄βontoββͺ (πΎ βΎt (πΉ β π΄))) |
23 | 3 | cnrest 22659 |
. . . 4
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ)) |
24 | 2, 8, 23 | syl2anc 585 |
. . 3
β’ (π β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ)) |
25 | | toptopon2 22290 |
. . . . 5
β’ (πΎ β Top β πΎ β (TopOnββͺ πΎ)) |
26 | 14, 25 | sylib 217 |
. . . 4
β’ (π β πΎ β (TopOnββͺ πΎ)) |
27 | | df-ima 5650 |
. . . . 5
β’ (πΉ β π΄) = ran (πΉ βΎ π΄) |
28 | | eqimss2 4005 |
. . . . 5
β’ ((πΉ β π΄) = ran (πΉ βΎ π΄) β ran (πΉ βΎ π΄) β (πΉ β π΄)) |
29 | 27, 28 | mp1i 13 |
. . . 4
β’ (π β ran (πΉ βΎ π΄) β (πΉ β π΄)) |
30 | | cnrest2 22660 |
. . . 4
β’ ((πΎ β (TopOnββͺ πΎ)
β§ ran (πΉ βΎ π΄) β (πΉ β π΄) β§ (πΉ β π΄) β βͺ πΎ) β ((πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (πΎ βΎt (πΉ β π΄))))) |
31 | 26, 29, 17, 30 | syl3anc 1372 |
. . 3
β’ (π β ((πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (πΎ βΎt (πΉ β π΄))))) |
32 | 24, 31 | mpbid 231 |
. 2
β’ (π β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (πΎ βΎt (πΉ β π΄)))) |
33 | | eqid 2733 |
. . 3
β’ βͺ (πΎ
βΎt (πΉ
β π΄)) = βͺ (πΎ
βΎt (πΉ
β π΄)) |
34 | 33 | cnconn 22796 |
. 2
β’ (((π½ βΎt π΄) β Conn β§ (πΉ βΎ π΄):π΄βontoββͺ (πΎ βΎt (πΉ β π΄)) β§ (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (πΎ βΎt (πΉ β π΄)))) β (πΎ βΎt (πΉ β π΄)) β Conn) |
35 | 1, 22, 32, 34 | syl3anc 1372 |
1
β’ (π β (πΎ βΎt (πΉ β π΄)) β Conn) |