Step | Hyp | Ref
| Expression |
1 | | qtopomap.5 |
. . 3
β’ (π β πΉ β (π½ Cn πΎ)) |
2 | | qtopomap.4 |
. . 3
β’ (π β πΎ β (TopOnβπ)) |
3 | | qtopomap.6 |
. . 3
β’ (π β ran πΉ = π) |
4 | | qtopss 23089 |
. . 3
β’ ((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β πΎ β (π½ qTop πΉ)) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. 2
β’ (π β πΎ β (π½ qTop πΉ)) |
6 | | cntop1 22614 |
. . . . . 6
β’ (πΉ β (π½ Cn πΎ) β π½ β Top) |
7 | 1, 6 | syl 17 |
. . . . 5
β’ (π β π½ β Top) |
8 | | toptopon2 22290 |
. . . . . . . . 9
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
9 | 7, 8 | sylib 217 |
. . . . . . . 8
β’ (π β π½ β (TopOnββͺ π½)) |
10 | | cnf2 22623 |
. . . . . . . 8
β’ ((π½ β (TopOnββͺ π½)
β§ πΎ β
(TopOnβπ) β§ πΉ β (π½ Cn πΎ)) β πΉ:βͺ π½βΆπ) |
11 | 9, 2, 1, 10 | syl3anc 1372 |
. . . . . . 7
β’ (π β πΉ:βͺ π½βΆπ) |
12 | 11 | ffnd 6673 |
. . . . . 6
β’ (π β πΉ Fn βͺ π½) |
13 | | df-fo 6506 |
. . . . . 6
β’ (πΉ:βͺ
π½βontoβπ β (πΉ Fn βͺ π½ β§ ran πΉ = π)) |
14 | 12, 3, 13 | sylanbrc 584 |
. . . . 5
β’ (π β πΉ:βͺ π½βontoβπ) |
15 | | eqid 2733 |
. . . . . 6
β’ βͺ π½ =
βͺ π½ |
16 | 15 | elqtop2 23075 |
. . . . 5
β’ ((π½ β Top β§ πΉ:βͺ
π½βontoβπ) β (π¦ β (π½ qTop πΉ) β (π¦ β π β§ (β‘πΉ β π¦) β π½))) |
17 | 7, 14, 16 | syl2anc 585 |
. . . 4
β’ (π β (π¦ β (π½ qTop πΉ) β (π¦ β π β§ (β‘πΉ β π¦) β π½))) |
18 | 14 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β πΉ:βͺ π½βontoβπ) |
19 | | difss 4095 |
. . . . . . . . 9
β’ (π β π¦) β π |
20 | | foimacnv 6805 |
. . . . . . . . 9
β’ ((πΉ:βͺ
π½βontoβπ β§ (π β π¦) β π) β (πΉ β (β‘πΉ β (π β π¦))) = (π β π¦)) |
21 | 18, 19, 20 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (πΉ β (β‘πΉ β (π β π¦))) = (π β π¦)) |
22 | 2 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β πΎ β (TopOnβπ)) |
23 | | toponuni 22286 |
. . . . . . . . . 10
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β π = βͺ πΎ) |
25 | 24 | difeq1d 4085 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (π β π¦) = (βͺ πΎ β π¦)) |
26 | 21, 25 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (πΉ β (β‘πΉ β (π β π¦))) = (βͺ πΎ β π¦)) |
27 | | imaeq2 6013 |
. . . . . . . . 9
β’ (π₯ = (β‘πΉ β (π β π¦)) β (πΉ β π₯) = (πΉ β (β‘πΉ β (π β π¦)))) |
28 | 27 | eleq1d 2819 |
. . . . . . . 8
β’ (π₯ = (β‘πΉ β (π β π¦)) β ((πΉ β π₯) β (ClsdβπΎ) β (πΉ β (β‘πΉ β (π β π¦))) β (ClsdβπΎ))) |
29 | | qtopcmap.7 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Clsdβπ½)) β (πΉ β π₯) β (ClsdβπΎ)) |
30 | 29 | ralrimiva 3140 |
. . . . . . . . 9
β’ (π β βπ₯ β (Clsdβπ½)(πΉ β π₯) β (ClsdβπΎ)) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β βπ₯ β (Clsdβπ½)(πΉ β π₯) β (ClsdβπΎ)) |
32 | | fofun 6761 |
. . . . . . . . . . 11
β’ (πΉ:βͺ
π½βontoβπ β Fun πΉ) |
33 | | funcnvcnv 6572 |
. . . . . . . . . . 11
β’ (Fun
πΉ β Fun β‘β‘πΉ) |
34 | | imadif 6589 |
. . . . . . . . . . 11
β’ (Fun
β‘β‘πΉ β (β‘πΉ β (π β π¦)) = ((β‘πΉ β π) β (β‘πΉ β π¦))) |
35 | 18, 32, 33, 34 | 4syl 19 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (β‘πΉ β (π β π¦)) = ((β‘πΉ β π) β (β‘πΉ β π¦))) |
36 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β πΉ:βͺ π½βΆπ) |
37 | | fimacnv 6694 |
. . . . . . . . . . . 12
β’ (πΉ:βͺ
π½βΆπ β (β‘πΉ β π) = βͺ π½) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (β‘πΉ β π) = βͺ π½) |
39 | 38 | difeq1d 4085 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β ((β‘πΉ β π) β (β‘πΉ β π¦)) = (βͺ π½ β (β‘πΉ β π¦))) |
40 | 35, 39 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (β‘πΉ β (π β π¦)) = (βͺ π½ β (β‘πΉ β π¦))) |
41 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β π½ β Top) |
42 | | simprr 772 |
. . . . . . . . . 10
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (β‘πΉ β π¦) β π½) |
43 | 15 | opncld 22407 |
. . . . . . . . . 10
β’ ((π½ β Top β§ (β‘πΉ β π¦) β π½) β (βͺ π½ β (β‘πΉ β π¦)) β (Clsdβπ½)) |
44 | 41, 42, 43 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (βͺ
π½ β (β‘πΉ β π¦)) β (Clsdβπ½)) |
45 | 40, 44 | eqeltrd 2834 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (β‘πΉ β (π β π¦)) β (Clsdβπ½)) |
46 | 28, 31, 45 | rspcdva 3584 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (πΉ β (β‘πΉ β (π β π¦))) β (ClsdβπΎ)) |
47 | 26, 46 | eqeltrrd 2835 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (βͺ
πΎ β π¦) β (ClsdβπΎ)) |
48 | | topontop 22285 |
. . . . . . . 8
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
49 | 22, 48 | syl 17 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β πΎ β Top) |
50 | | simprl 770 |
. . . . . . . 8
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β π¦ β π) |
51 | 50, 24 | sseqtrd 3988 |
. . . . . . 7
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β π¦ β βͺ πΎ) |
52 | | eqid 2733 |
. . . . . . . 8
β’ βͺ πΎ =
βͺ πΎ |
53 | 52 | isopn2 22406 |
. . . . . . 7
β’ ((πΎ β Top β§ π¦ β βͺ πΎ)
β (π¦ β πΎ β (βͺ πΎ
β π¦) β
(ClsdβπΎ))) |
54 | 49, 51, 53 | syl2anc 585 |
. . . . . 6
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β (π¦ β πΎ β (βͺ πΎ β π¦) β (ClsdβπΎ))) |
55 | 47, 54 | mpbird 257 |
. . . . 5
β’ ((π β§ (π¦ β π β§ (β‘πΉ β π¦) β π½)) β π¦ β πΎ) |
56 | 55 | ex 414 |
. . . 4
β’ (π β ((π¦ β π β§ (β‘πΉ β π¦) β π½) β π¦ β πΎ)) |
57 | 17, 56 | sylbid 239 |
. . 3
β’ (π β (π¦ β (π½ qTop πΉ) β π¦ β πΎ)) |
58 | 57 | ssrdv 3954 |
. 2
β’ (π β (π½ qTop πΉ) β πΎ) |
59 | 5, 58 | eqssd 3965 |
1
β’ (π β πΎ = (π½ qTop πΉ)) |