Step | Hyp | Ref
| Expression |
1 | | simp3l 1202 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β πΉ β (π½ Cn πΎ)) |
2 | | simp2l 1200 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β π΄ β π) |
3 | | cnres2.1 |
. . . 4
β’ π = βͺ
π½ |
4 | 3 | cnrest 22789 |
. . 3
β’ ((πΉ β (π½ Cn πΎ) β§ π΄ β π) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ)) |
5 | 1, 2, 4 | syl2anc 585 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ)) |
6 | | simp1r 1199 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β πΎ β Top) |
7 | | cnres2.2 |
. . . . 5
β’ π = βͺ
πΎ |
8 | 7 | toptopon 22419 |
. . . 4
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
9 | 6, 8 | sylib 217 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β πΎ β (TopOnβπ)) |
10 | | df-ima 5690 |
. . . 4
β’ (πΉ β π΄) = ran (πΉ βΎ π΄) |
11 | | simp3r 1203 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β βπ₯ β π΄ (πΉβπ₯) β π΅) |
12 | 3, 7 | cnf 22750 |
. . . . . . 7
β’ (πΉ β (π½ Cn πΎ) β πΉ:πβΆπ) |
13 | | ffun 6721 |
. . . . . . 7
β’ (πΉ:πβΆπ β Fun πΉ) |
14 | 1, 12, 13 | 3syl 18 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β Fun πΉ) |
15 | | fdm 6727 |
. . . . . . . 8
β’ (πΉ:πβΆπ β dom πΉ = π) |
16 | 1, 12, 15 | 3syl 18 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β dom πΉ = π) |
17 | 2, 16 | sseqtrrd 4024 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β π΄ β dom πΉ) |
18 | | funimass4 6957 |
. . . . . 6
β’ ((Fun
πΉ β§ π΄ β dom πΉ) β ((πΉ β π΄) β π΅ β βπ₯ β π΄ (πΉβπ₯) β π΅)) |
19 | 14, 17, 18 | syl2anc 585 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β ((πΉ β π΄) β π΅ β βπ₯ β π΄ (πΉβπ₯) β π΅)) |
20 | 11, 19 | mpbird 257 |
. . . 4
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β (πΉ β π΄) β π΅) |
21 | 10, 20 | eqsstrrid 4032 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β ran (πΉ βΎ π΄) β π΅) |
22 | | simp2r 1201 |
. . 3
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β π΅ β π) |
23 | | cnrest2 22790 |
. . 3
β’ ((πΎ β (TopOnβπ) β§ ran (πΉ βΎ π΄) β π΅ β§ π΅ β π) β ((πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (πΎ βΎt π΅)))) |
24 | 9, 21, 22, 23 | syl3anc 1372 |
. 2
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β ((πΉ βΎ π΄) β ((π½ βΎt π΄) Cn πΎ) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (πΎ βΎt π΅)))) |
25 | 5, 24 | mpbid 231 |
1
β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β π β§ π΅ β π) β§ (πΉ β (π½ Cn πΎ) β§ βπ₯ β π΄ (πΉβπ₯) β π΅)) β (πΉ βΎ π΄) β ((π½ βΎt π΄) Cn (πΎ βΎt π΅))) |