Step | Hyp | Ref
| Expression |
1 | | cnf2 22973 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:πβΆπ) |
2 | 1 | 3expa 1116 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β (π½ Cn πΎ)) β πΉ:πβΆπ) |
3 | | cnclima 22992 |
. . . . 5
β’ ((πΉ β (π½ Cn πΎ) β§ π¦ β (ClsdβπΎ)) β (β‘πΉ β π¦) β (Clsdβπ½)) |
4 | 3 | ralrimiva 3144 |
. . . 4
β’ (πΉ β (π½ Cn πΎ) β βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½)) |
5 | 4 | adantl 480 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β (π½ Cn πΎ)) β βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½)) |
6 | 2, 5 | jca 510 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β (π½ Cn πΎ)) β (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) |
7 | | simprl 767 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β πΉ:πβΆπ) |
8 | | toponuni 22636 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
9 | 8 | ad3antrrr 726 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β π = βͺ π½) |
10 | | simplrl 773 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β πΉ:πβΆπ) |
11 | | fimacnv 6738 |
. . . . . . . . . . 11
β’ (πΉ:πβΆπ β (β‘πΉ β π) = π) |
12 | 11 | eqcomd 2736 |
. . . . . . . . . 10
β’ (πΉ:πβΆπ β π = (β‘πΉ β π)) |
13 | 10, 12 | syl 17 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β π = (β‘πΉ β π)) |
14 | 9, 13 | eqtr3d 2772 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β βͺ π½ = (β‘πΉ β π)) |
15 | 14 | difeq1d 4120 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (βͺ π½ β (β‘πΉ β π₯)) = ((β‘πΉ β π) β (β‘πΉ β π₯))) |
16 | | ffun 6719 |
. . . . . . . 8
β’ (πΉ:πβΆπ β Fun πΉ) |
17 | | funcnvcnv 6614 |
. . . . . . . 8
β’ (Fun
πΉ β Fun β‘β‘πΉ) |
18 | | imadif 6631 |
. . . . . . . 8
β’ (Fun
β‘β‘πΉ β (β‘πΉ β (π β π₯)) = ((β‘πΉ β π) β (β‘πΉ β π₯))) |
19 | 10, 16, 17, 18 | 4syl 19 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β (π β π₯)) = ((β‘πΉ β π) β (β‘πΉ β π₯))) |
20 | 15, 19 | eqtr4d 2773 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (βͺ π½ β (β‘πΉ β π₯)) = (β‘πΉ β (π β π₯))) |
21 | | imaeq2 6054 |
. . . . . . . 8
β’ (π¦ = (π β π₯) β (β‘πΉ β π¦) = (β‘πΉ β (π β π₯))) |
22 | 21 | eleq1d 2816 |
. . . . . . 7
β’ (π¦ = (π β π₯) β ((β‘πΉ β π¦) β (Clsdβπ½) β (β‘πΉ β (π β π₯)) β (Clsdβπ½))) |
23 | | simplrr 774 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½)) |
24 | | toponuni 22636 |
. . . . . . . . . 10
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
25 | 24 | ad3antlr 727 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β π = βͺ πΎ) |
26 | 25 | difeq1d 4120 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (π β π₯) = (βͺ πΎ β π₯)) |
27 | | topontop 22635 |
. . . . . . . . . 10
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
28 | 27 | ad3antlr 727 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β πΎ β Top) |
29 | | eqid 2730 |
. . . . . . . . . 10
β’ βͺ πΎ =
βͺ πΎ |
30 | 29 | opncld 22757 |
. . . . . . . . 9
β’ ((πΎ β Top β§ π₯ β πΎ) β (βͺ πΎ β π₯) β (ClsdβπΎ)) |
31 | 28, 30 | sylancom 586 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (βͺ πΎ β π₯) β (ClsdβπΎ)) |
32 | 26, 31 | eqeltrd 2831 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (π β π₯) β (ClsdβπΎ)) |
33 | 22, 23, 32 | rspcdva 3612 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β (π β π₯)) β (Clsdβπ½)) |
34 | 20, 33 | eqeltrd 2831 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (βͺ π½ β (β‘πΉ β π₯)) β (Clsdβπ½)) |
35 | | topontop 22635 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π½ β Top) |
36 | 35 | ad3antrrr 726 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β π½ β Top) |
37 | | cnvimass 6079 |
. . . . . . . 8
β’ (β‘πΉ β π₯) β dom πΉ |
38 | 37, 10 | fssdm 6736 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β π₯) β π) |
39 | 38, 9 | sseqtrd 4021 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β π₯) β βͺ π½) |
40 | | eqid 2730 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
41 | 40 | isopn2 22756 |
. . . . . 6
β’ ((π½ β Top β§ (β‘πΉ β π₯) β βͺ π½) β ((β‘πΉ β π₯) β π½ β (βͺ π½ β (β‘πΉ β π₯)) β (Clsdβπ½))) |
42 | 36, 39, 41 | syl2anc 582 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β ((β‘πΉ β π₯) β π½ β (βͺ π½ β (β‘πΉ β π₯)) β (Clsdβπ½))) |
43 | 34, 42 | mpbird 256 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β§ π₯ β πΎ) β (β‘πΉ β π₯) β π½) |
44 | 43 | ralrimiva 3144 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β βπ₯ β πΎ (β‘πΉ β π₯) β π½) |
45 | | iscn 22959 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β πΎ (β‘πΉ β π₯) β π½))) |
46 | 45 | adantr 479 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ₯ β πΎ (β‘πΉ β π₯) β π½))) |
47 | 7, 44, 46 | mpbir2and 709 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½))) β πΉ β (π½ Cn πΎ)) |
48 | 6, 47 | impbida 797 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ¦ β (ClsdβπΎ)(β‘πΉ β π¦) β (Clsdβπ½)))) |