Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . 6
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
2 | 1 | kqffn 23449 |
. . . . 5
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
3 | 2 | 3ad2ant1 1133 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β πΉ Fn π) |
4 | | fncnvima2 7062 |
. . . 4
β’ (πΉ Fn π β (β‘πΉ β {(πΉβπ΄)}) = {π§ β π β£ (πΉβπ§) β {(πΉβπ΄)}}) |
5 | 3, 4 | syl 17 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β (β‘πΉ β {(πΉβπ΄)}) = {π§ β π β£ (πΉβπ§) β {(πΉβπ΄)}}) |
6 | | fvex 6904 |
. . . . . 6
β’ (πΉβπ§) β V |
7 | 6 | elsn 4643 |
. . . . 5
β’ ((πΉβπ§) β {(πΉβπ΄)} β (πΉβπ§) = (πΉβπ΄)) |
8 | | simpl1 1191 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β§ π§ β π) β π½ β (TopOnβπ)) |
9 | | simpr 485 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β§ π§ β π) β π§ β π) |
10 | | simpl3 1193 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β§ π§ β π) β π΄ β π) |
11 | 1 | kqfeq 23448 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π΄ β π) β ((πΉβπ§) = (πΉβπ΄) β βπ¦ β π½ (π§ β π¦ β π΄ β π¦))) |
12 | | eleq2w 2817 |
. . . . . . . . 9
β’ (π¦ = π β (π§ β π¦ β π§ β π)) |
13 | | eleq2w 2817 |
. . . . . . . . 9
β’ (π¦ = π β (π΄ β π¦ β π΄ β π)) |
14 | 12, 13 | bibi12d 345 |
. . . . . . . 8
β’ (π¦ = π β ((π§ β π¦ β π΄ β π¦) β (π§ β π β π΄ β π))) |
15 | 14 | cbvralvw 3234 |
. . . . . . 7
β’
(βπ¦ β
π½ (π§ β π¦ β π΄ β π¦) β βπ β π½ (π§ β π β π΄ β π)) |
16 | 11, 15 | bitrdi 286 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π΄ β π) β ((πΉβπ§) = (πΉβπ΄) β βπ β π½ (π§ β π β π΄ β π))) |
17 | 8, 9, 10, 16 | syl3anc 1371 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β§ π§ β π) β ((πΉβπ§) = (πΉβπ΄) β βπ β π½ (π§ β π β π΄ β π))) |
18 | 7, 17 | bitrid 282 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β§ π§ β π) β ((πΉβπ§) β {(πΉβπ΄)} β βπ β π½ (π§ β π β π΄ β π))) |
19 | 18 | rabbidva 3439 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β {π§ β π β£ (πΉβπ§) β {(πΉβπ΄)}} = {π§ β π β£ βπ β π½ (π§ β π β π΄ β π)}) |
20 | 5, 19 | eqtrd 2772 |
. 2
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β (β‘πΉ β {(πΉβπ΄)}) = {π§ β π β£ βπ β π½ (π§ β π β π΄ β π)}) |
21 | 1 | kqid 23452 |
. . . 4
β’ (π½ β (TopOnβπ) β πΉ β (π½ Cn (KQβπ½))) |
22 | 21 | 3ad2ant1 1133 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β πΉ β (π½ Cn (KQβπ½))) |
23 | | simp2 1137 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β (KQβπ½) β Fre) |
24 | | simp3 1138 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β π΄ β π) |
25 | | fnfvelrn 7082 |
. . . . . 6
β’ ((πΉ Fn π β§ π΄ β π) β (πΉβπ΄) β ran πΉ) |
26 | 3, 24, 25 | syl2anc 584 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β (πΉβπ΄) β ran πΉ) |
27 | 1 | kqtopon 23451 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β (KQβπ½) β (TopOnβran πΉ)) |
28 | 27 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β (KQβπ½) β (TopOnβran πΉ)) |
29 | | toponuni 22636 |
. . . . . 6
β’
((KQβπ½) β
(TopOnβran πΉ) β
ran πΉ = βͺ (KQβπ½)) |
30 | 28, 29 | syl 17 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β ran πΉ = βͺ
(KQβπ½)) |
31 | 26, 30 | eleqtrd 2835 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β (πΉβπ΄) β βͺ
(KQβπ½)) |
32 | | eqid 2732 |
. . . . 5
β’ βͺ (KQβπ½) = βͺ
(KQβπ½) |
33 | 32 | t1sncld 23050 |
. . . 4
β’
(((KQβπ½)
β Fre β§ (πΉβπ΄) β βͺ
(KQβπ½)) β
{(πΉβπ΄)} β (Clsdβ(KQβπ½))) |
34 | 23, 31, 33 | syl2anc 584 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β {(πΉβπ΄)} β (Clsdβ(KQβπ½))) |
35 | | cnclima 22992 |
. . 3
β’ ((πΉ β (π½ Cn (KQβπ½)) β§ {(πΉβπ΄)} β (Clsdβ(KQβπ½))) β (β‘πΉ β {(πΉβπ΄)}) β (Clsdβπ½)) |
36 | 22, 34, 35 | syl2anc 584 |
. 2
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β (β‘πΉ β {(πΉβπ΄)}) β (Clsdβπ½)) |
37 | 20, 36 | eqeltrrd 2834 |
1
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre β§ π΄ β π) β {π§ β π β£ βπ β π½ (π§ β π β π΄ β π)} β (Clsdβπ½)) |