Step | Hyp | Ref
| Expression |
1 | | imadmres 6187 |
. . . . 5
β’ (πΉ β dom (πΉ βΎ (π΄ β π))) = (πΉ β (π΄ β π)) |
2 | | dmres 5960 |
. . . . . . 7
β’ dom
(πΉ βΎ (π΄ β π)) = ((π΄ β π) β© dom πΉ) |
3 | | kqval.2 |
. . . . . . . . . . 11
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
4 | 3 | kqffn 23092 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
5 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π β π½) β πΉ Fn π) |
6 | 5 | fndmd 6608 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π β π½) β dom πΉ = π) |
7 | 6 | ineq2d 4173 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π½) β ((π΄ β π) β© dom πΉ) = ((π΄ β π) β© π)) |
8 | 2, 7 | eqtrid 2785 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π β π½) β dom (πΉ βΎ (π΄ β π)) = ((π΄ β π) β© π)) |
9 | 8 | imaeq2d 6014 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π β π½) β (πΉ β dom (πΉ βΎ (π΄ β π))) = (πΉ β ((π΄ β π) β© π))) |
10 | 1, 9 | eqtr3id 2787 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β π½) β (πΉ β (π΄ β π)) = (πΉ β ((π΄ β π) β© π))) |
11 | | indif1 4232 |
. . . . . 6
β’ ((π΄ β π) β© π) = ((π΄ β© π) β π) |
12 | | inss2 4190 |
. . . . . . 7
β’ (π΄ β© π) β π |
13 | | ssdif 4100 |
. . . . . . 7
β’ ((π΄ β© π) β π β ((π΄ β© π) β π) β (π β π)) |
14 | 12, 13 | ax-mp 5 |
. . . . . 6
β’ ((π΄ β© π) β π) β (π β π) |
15 | 11, 14 | eqsstri 3979 |
. . . . 5
β’ ((π΄ β π) β© π) β (π β π) |
16 | | imass2 6055 |
. . . . 5
β’ (((π΄ β π) β© π) β (π β π) β (πΉ β ((π΄ β π) β© π)) β (πΉ β (π β π))) |
17 | 15, 16 | mp1i 13 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β π½) β (πΉ β ((π΄ β π) β© π)) β (πΉ β (π β π))) |
18 | 10, 17 | eqsstrd 3983 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π½) β (πΉ β (π΄ β π)) β (πΉ β (π β π))) |
19 | | sslin 4195 |
. . 3
β’ ((πΉ β (π΄ β π)) β (πΉ β (π β π)) β ((πΉ β π) β© (πΉ β (π΄ β π))) β ((πΉ β π) β© (πΉ β (π β π)))) |
20 | 18, 19 | syl 17 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β π½) β ((πΉ β π) β© (πΉ β (π΄ β π))) β ((πΉ β π) β© (πΉ β (π β π)))) |
21 | | eldifn 4088 |
. . . . . . 7
β’ (π€ β (π β π) β Β¬ π€ β π) |
22 | 21 | adantl 483 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π β π½) β§ π€ β (π β π)) β Β¬ π€ β π) |
23 | | simpll 766 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π β π½) β§ π€ β (π β π)) β π½ β (TopOnβπ)) |
24 | | simplr 768 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π β π½) β§ π€ β (π β π)) β π β π½) |
25 | | eldifi 4087 |
. . . . . . . 8
β’ (π€ β (π β π) β π€ β π) |
26 | 25 | adantl 483 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π β π½) β§ π€ β (π β π)) β π€ β π) |
27 | 3 | kqfvima 23097 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π€ β π) β (π€ β π β (πΉβπ€) β (πΉ β π))) |
28 | 23, 24, 26, 27 | syl3anc 1372 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π β π½) β§ π€ β (π β π)) β (π€ β π β (πΉβπ€) β (πΉ β π))) |
29 | 22, 28 | mtbid 324 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π β π½) β§ π€ β (π β π)) β Β¬ (πΉβπ€) β (πΉ β π)) |
30 | 29 | ralrimiva 3140 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β π½) β βπ€ β (π β π) Β¬ (πΉβπ€) β (πΉ β π)) |
31 | | difss 4092 |
. . . . 5
β’ (π β π) β π |
32 | | eleq1 2822 |
. . . . . . 7
β’ (π§ = (πΉβπ€) β (π§ β (πΉ β π) β (πΉβπ€) β (πΉ β π))) |
33 | 32 | notbid 318 |
. . . . . 6
β’ (π§ = (πΉβπ€) β (Β¬ π§ β (πΉ β π) β Β¬ (πΉβπ€) β (πΉ β π))) |
34 | 33 | ralima 7189 |
. . . . 5
β’ ((πΉ Fn π β§ (π β π) β π) β (βπ§ β (πΉ β (π β π)) Β¬ π§ β (πΉ β π) β βπ€ β (π β π) Β¬ (πΉβπ€) β (πΉ β π))) |
35 | 5, 31, 34 | sylancl 587 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β π½) β (βπ§ β (πΉ β (π β π)) Β¬ π§ β (πΉ β π) β βπ€ β (π β π) Β¬ (πΉβπ€) β (πΉ β π))) |
36 | 30, 35 | mpbird 257 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π½) β βπ§ β (πΉ β (π β π)) Β¬ π§ β (πΉ β π)) |
37 | | disjr 4410 |
. . 3
β’ (((πΉ β π) β© (πΉ β (π β π))) = β
β βπ§ β (πΉ β (π β π)) Β¬ π§ β (πΉ β π)) |
38 | 36, 37 | sylibr 233 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β π½) β ((πΉ β π) β© (πΉ β (π β π))) = β
) |
39 | | sseq0 4360 |
. 2
β’ ((((πΉ β π) β© (πΉ β (π΄ β π))) β ((πΉ β π) β© (πΉ β (π β π))) β§ ((πΉ β π) β© (πΉ β (π β π))) = β
) β ((πΉ β π) β© (πΉ β (π΄ β π))) = β
) |
40 | 20, 38, 39 | syl2anc 585 |
1
β’ ((π½ β (TopOnβπ) β§ π β π½) β ((πΉ β π) β© (πΉ β (π΄ β π))) = β
) |