Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . 7
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
2 | 1 | kqffn 23229 |
. . . . . 6
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
3 | | elpreima 7060 |
. . . . . 6
β’ (πΉ Fn π β (π§ β (β‘πΉ β (πΉ β π)) β (π§ β π β§ (πΉβπ§) β (πΉ β π)))) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ (π½ β (TopOnβπ) β (π§ β (β‘πΉ β (πΉ β π)) β (π§ β π β§ (πΉβπ§) β (πΉ β π)))) |
5 | 4 | adantr 482 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (π§ β (β‘πΉ β (πΉ β π)) β (π§ β π β§ (πΉβπ§) β (πΉ β π)))) |
6 | | noel 4331 |
. . . . . . . 8
β’ Β¬
(πΉβπ§) β β
|
7 | | elin 3965 |
. . . . . . . . 9
β’ ((πΉβπ§) β ((πΉ β π) β© (πΉ β (π β π))) β ((πΉβπ§) β (πΉ β π) β§ (πΉβπ§) β (πΉ β (π β π)))) |
8 | | incom 4202 |
. . . . . . . . . . 11
β’ ((πΉ β π) β© (πΉ β (π β π))) = ((πΉ β (π β π)) β© (πΉ β π)) |
9 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
β’ βͺ π½ =
βͺ π½ |
10 | 9 | cldss 22533 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (Clsdβπ½) β π β βͺ π½) |
11 | 10 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β π β βͺ π½) |
12 | | fndm 6653 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΉ Fn π β dom πΉ = π) |
13 | 2, 12 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π½ β (TopOnβπ) β dom πΉ = π) |
14 | | toponuni 22416 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
15 | 13, 14 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . 19
β’ (π½ β (TopOnβπ) β dom πΉ = βͺ π½) |
16 | 15 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β dom πΉ = βͺ π½) |
17 | 11, 16 | sseqtrrd 4024 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β π β dom πΉ) |
18 | 13 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β dom πΉ = π) |
19 | 17, 18 | sseqtrd 4023 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β π β π) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β π β π) |
21 | | dfss4 4259 |
. . . . . . . . . . . . . . 15
β’ (π β π β (π β (π β π)) = π) |
22 | 20, 21 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β (π β (π β π)) = π) |
23 | 22 | imaeq2d 6060 |
. . . . . . . . . . . . 13
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β (πΉ β (π β (π β π))) = (πΉ β π)) |
24 | 23 | ineq2d 4213 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β ((πΉ β (π β π)) β© (πΉ β (π β (π β π)))) = ((πΉ β (π β π)) β© (πΉ β π))) |
25 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β π½ β (TopOnβπ)) |
26 | 14 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β π = βͺ π½) |
27 | 26 | difeq1d 4122 |
. . . . . . . . . . . . . . 15
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (π β π) = (βͺ π½ β π)) |
28 | 9 | cldopn 22535 |
. . . . . . . . . . . . . . . 16
β’ (π β (Clsdβπ½) β (βͺ π½
β π) β π½) |
29 | 28 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (βͺ
π½ β π) β π½) |
30 | 27, 29 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (π β π) β π½) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β (π β π) β π½) |
32 | 1 | kqdisj 23236 |
. . . . . . . . . . . . 13
β’ ((π½ β (TopOnβπ) β§ (π β π) β π½) β ((πΉ β (π β π)) β© (πΉ β (π β (π β π)))) = β
) |
33 | 25, 31, 32 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β ((πΉ β (π β π)) β© (πΉ β (π β (π β π)))) = β
) |
34 | 24, 33 | eqtr3d 2775 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β ((πΉ β (π β π)) β© (πΉ β π)) = β
) |
35 | 8, 34 | eqtrid 2785 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β ((πΉ β π) β© (πΉ β (π β π))) = β
) |
36 | 35 | eleq2d 2820 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β ((πΉβπ§) β ((πΉ β π) β© (πΉ β (π β π))) β (πΉβπ§) β β
)) |
37 | 7, 36 | bitr3id 285 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β (((πΉβπ§) β (πΉ β π) β§ (πΉβπ§) β (πΉ β (π β π))) β (πΉβπ§) β β
)) |
38 | 6, 37 | mtbiri 327 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β Β¬ ((πΉβπ§) β (πΉ β π) β§ (πΉβπ§) β (πΉ β (π β π)))) |
39 | | imnan 401 |
. . . . . . 7
β’ (((πΉβπ§) β (πΉ β π) β Β¬ (πΉβπ§) β (πΉ β (π β π))) β Β¬ ((πΉβπ§) β (πΉ β π) β§ (πΉβπ§) β (πΉ β (π β π)))) |
40 | 38, 39 | sylibr 233 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β ((πΉβπ§) β (πΉ β π) β Β¬ (πΉβπ§) β (πΉ β (π β π)))) |
41 | | eldif 3959 |
. . . . . . . . . 10
β’ (π§ β (π β π) β (π§ β π β§ Β¬ π§ β π)) |
42 | 41 | baibr 538 |
. . . . . . . . 9
β’ (π§ β π β (Β¬ π§ β π β π§ β (π β π))) |
43 | 42 | adantl 483 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β (Β¬ π§ β π β π§ β (π β π))) |
44 | | simpr 486 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β π§ β π) |
45 | 1 | kqfvima 23234 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ (π β π) β π½ β§ π§ β π) β (π§ β (π β π) β (πΉβπ§) β (πΉ β (π β π)))) |
46 | 25, 31, 44, 45 | syl3anc 1372 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β (π§ β (π β π) β (πΉβπ§) β (πΉ β (π β π)))) |
47 | 43, 46 | bitrd 279 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β (Β¬ π§ β π β (πΉβπ§) β (πΉ β (π β π)))) |
48 | 47 | con1bid 356 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β (Β¬ (πΉβπ§) β (πΉ β (π β π)) β π§ β π)) |
49 | 40, 48 | sylibd 238 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β§ π§ β π) β ((πΉβπ§) β (πΉ β π) β π§ β π)) |
50 | 49 | expimpd 455 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β ((π§ β π β§ (πΉβπ§) β (πΉ β π)) β π§ β π)) |
51 | 5, 50 | sylbid 239 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (π§ β (β‘πΉ β (πΉ β π)) β π§ β π)) |
52 | 51 | ssrdv 3989 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (β‘πΉ β (πΉ β π)) β π) |
53 | | sseqin2 4216 |
. . . 4
β’ (π β dom πΉ β (dom πΉ β© π) = π) |
54 | 17, 53 | sylib 217 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (dom πΉ β© π) = π) |
55 | | dminss 6153 |
. . 3
β’ (dom
πΉ β© π) β (β‘πΉ β (πΉ β π)) |
56 | 54, 55 | eqsstrrdi 4038 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β π β (β‘πΉ β (πΉ β π))) |
57 | 52, 56 | eqssd 4000 |
1
β’ ((π½ β (TopOnβπ) β§ π β (Clsdβπ½)) β (β‘πΉ β (πΉ β π)) = π) |