Step | Hyp | Ref
| Expression |
1 | | imassrn 6071 |
. . . 4
β’ (πΉ β π) β ran πΉ |
2 | 1 | a1i 11 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (πΉ β π) β ran πΉ) |
3 | | kqval.2 |
. . . . 5
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
4 | 3 | kqcldsat 23237 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (β‘πΉ β (πΉ β π)) = π) |
5 | | simpr 486 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β π β (Clsdβπ½)) |
6 | 4, 5 | eqeltrd 2834 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (β‘πΉ β (πΉ β π)) β (Clsdβπ½)) |
7 | 3 | kqffn 23229 |
. . . . . 6
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
8 | | dffn4 6812 |
. . . . . 6
β’ (πΉ Fn π β πΉ:πβontoβran πΉ) |
9 | 7, 8 | sylib 217 |
. . . . 5
β’ (π½ β (TopOnβπ) β πΉ:πβontoβran πΉ) |
10 | | qtopcld 23217 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβran πΉ) β ((πΉ β π) β (Clsdβ(π½ qTop πΉ)) β ((πΉ β π) β ran πΉ β§ (β‘πΉ β (πΉ β π)) β (Clsdβπ½)))) |
11 | 9, 10 | mpdan 686 |
. . . 4
β’ (π½ β (TopOnβπ) β ((πΉ β π) β (Clsdβ(π½ qTop πΉ)) β ((πΉ β π) β ran πΉ β§ (β‘πΉ β (πΉ β π)) β (Clsdβπ½)))) |
12 | 11 | adantr 482 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β ((πΉ β π) β (Clsdβ(π½ qTop πΉ)) β ((πΉ β π) β ran πΉ β§ (β‘πΉ β (πΉ β π)) β (Clsdβπ½)))) |
13 | 2, 6, 12 | mpbir2and 712 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (πΉ β π) β (Clsdβ(π½ qTop πΉ))) |
14 | 3 | kqval 23230 |
. . . 4
β’ (π½ β (TopOnβπ) β (KQβπ½) = (π½ qTop πΉ)) |
15 | 14 | adantr 482 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (KQβπ½) = (π½ qTop πΉ)) |
16 | 15 | fveq2d 6896 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (Clsdβ(KQβπ½)) = (Clsdβ(π½ qTop πΉ))) |
17 | 13, 16 | eleqtrrd 2837 |
1
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (πΉ β π) β (Clsdβ(KQβπ½))) |