Step | Hyp | Ref
| Expression |
1 | | cnf2 22753 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:πβΆπ) |
2 | 1 | 3expa 1119 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β (π½ Cn πΎ)) β πΉ:πβΆπ) |
3 | | cnclima 22772 |
. . . . 5
β’ ((πΉ β (π½ Cn πΎ) β§ π¦ β (ClsdβπΎ)) β (β‘πΉ β π¦) β (Clsdβπ½)) |
4 | 3 | ralrimiva 3147 |
. . . 4
β’ (πΉ β (π½ Cn πΎ) β βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½)) |
5 | 4 | adantl 483 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β (π½ Cn πΎ)) β βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½)) |
6 | 2, 5 | jca 513 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β (π½ Cn πΎ)) β (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) |
7 | | simprl 770 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β πΉ:πβΆπ) |
8 | | toponuni 22416 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
9 | 8 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β π = βͺ π½) |
10 | | simplrl 776 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β πΉ:πβΆπ) |
11 | | fimacnv 6740 |
. . . . . . . . . . 11
β’ (πΉ:πβΆπ β (β‘πΉ β π) = π) |
12 | 11 | eqcomd 2739 |
. . . . . . . . . 10
β’ (πΉ:πβΆπ β π = (β‘πΉ β π)) |
13 | 10, 12 | syl 17 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β π = (β‘πΉ β π)) |
14 | 9, 13 | eqtr3d 2775 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β βͺ π½ = (β‘πΉ β π)) |
15 | 14 | difeq1d 4122 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (βͺ π½ β (β‘πΉ β π₯)) = ((β‘πΉ β π) β (β‘πΉ β π₯))) |
16 | | ffun 6721 |
. . . . . . . 8
β’ (πΉ:πβΆπ β Fun πΉ) |
17 | | funcnvcnv 6616 |
. . . . . . . 8
β’ (Fun
πΉ β Fun β‘β‘πΉ) |
18 | | imadif 6633 |
. . . . . . . 8
β’ (Fun
β‘β‘πΉ β (β‘πΉ β (π β π₯)) = ((β‘πΉ β π) β (β‘πΉ β π₯))) |
19 | 10, 16, 17, 18 | 4syl 19 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β (π β π₯)) = ((β‘πΉ β π) β (β‘πΉ β π₯))) |
20 | 15, 19 | eqtr4d 2776 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (βͺ π½ β (β‘πΉ β π₯)) = (β‘πΉ β (π β π₯))) |
21 | | imaeq2 6056 |
. . . . . . . 8
β’ (π¦ = (π β π₯) β (β‘πΉ β π¦) = (β‘πΉ β (π β π₯))) |
22 | 21 | eleq1d 2819 |
. . . . . . 7
β’ (π¦ = (π β π₯) β ((β‘πΉ β π¦) β (Clsdβπ½) β (β‘πΉ β (π β π₯)) β (Clsdβπ½))) |
23 | | simplrr 777 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½)) |
24 | | toponuni 22416 |
. . . . . . . . . 10
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
25 | 24 | ad3antlr 730 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β π = βͺ πΎ) |
26 | 25 | difeq1d 4122 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (π β π₯) = (βͺ πΎ β π₯)) |
27 | | topontop 22415 |
. . . . . . . . . 10
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
28 | 27 | ad3antlr 730 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β πΎ β Top) |
29 | | eqid 2733 |
. . . . . . . . . 10
β’ βͺ πΎ =
βͺ πΎ |
30 | 29 | opncld 22537 |
. . . . . . . . 9
β’ ((πΎ β Top β§ π₯ β πΎ) β (βͺ πΎ β π₯) β (ClsdβπΎ)) |
31 | 28, 30 | sylancom 589 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (βͺ πΎ β π₯) β (ClsdβπΎ)) |
32 | 26, 31 | eqeltrd 2834 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (π β π₯) β (ClsdβπΎ)) |
33 | 22, 23, 32 | rspcdva 3614 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β (π β π₯)) β (Clsdβπ½)) |
34 | 20, 33 | eqeltrd 2834 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (βͺ π½ β (β‘πΉ β π₯)) β (Clsdβπ½)) |
35 | | topontop 22415 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π½ β Top) |
36 | 35 | ad3antrrr 729 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β π½ β Top) |
37 | | cnvimass 6081 |
. . . . . . . 8
β’ (β‘πΉ β π₯) β dom πΉ |
38 | 37, 10 | fssdm 6738 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β π₯) β π) |
39 | 38, 9 | sseqtrd 4023 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β π₯) β βͺ π½) |
40 | | eqid 2733 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
41 | 40 | isopn2 22536 |
. . . . . 6
β’ ((π½ β Top β§ (β‘πΉ β π₯) β βͺ π½) β ((β‘πΉ β π₯) β π½ β (βͺ π½ β (β‘πΉ β π₯)) β (Clsdβπ½))) |
42 | 36, 39, 41 | syl2anc 585 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β ((β‘πΉ β π₯) β π½ β (βͺ π½ β (β‘πΉ β π₯)) β (Clsdβπ½))) |
43 | 34, 42 | mpbird 257 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β π₯) β π½) |
44 | 43 | ralrimiva 3147 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β βπ₯ β πΎ (β‘πΉ β π₯) β π½) |
45 | | iscn 22739 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β πΎ (β‘πΉ β π₯) β π½))) |
46 | 45 | adantr 482 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β πΎ (β‘πΉ β π₯) β π½))) |
47 | 7, 44, 46 | mpbir2and 712 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β πΉ β (π½ Cn πΎ)) |
48 | 6, 47 | impbida 800 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½)))) |