Step | Hyp | Ref
| Expression |
1 | | regr1lem.3 |
. . . . 5
β’ (π β π½ β Reg) |
2 | 1 | adantr 481 |
. . . 4
β’ ((π β§ π΄ β π) β π½ β Reg) |
3 | | regr1lem.6 |
. . . . 5
β’ (π β π β π½) |
4 | 3 | adantr 481 |
. . . 4
β’ ((π β§ π΄ β π) β π β π½) |
5 | | simpr 485 |
. . . 4
β’ ((π β§ π΄ β π) β π΄ β π) |
6 | | regsep 22829 |
. . . 4
β’ ((π½ β Reg β§ π β π½ β§ π΄ β π) β βπ§ β π½ (π΄ β π§ β§ ((clsβπ½)βπ§) β π)) |
7 | 2, 4, 5, 6 | syl3anc 1371 |
. . 3
β’ ((π β§ π΄ β π) β βπ§ β π½ (π΄ β π§ β§ ((clsβπ½)βπ§) β π)) |
8 | | regr1lem.7 |
. . . . 5
β’ (π β Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
)) |
9 | 8 | ad2antrr 724 |
. . . 4
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
)) |
10 | | regr1lem.2 |
. . . . . . . 8
β’ (π β π½ β (TopOnβπ)) |
11 | 10 | ad3antrrr 728 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π½ β (TopOnβπ)) |
12 | | simplrl 775 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π§ β π½) |
13 | | kqval.2 |
. . . . . . . 8
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
14 | 13 | kqopn 23229 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π§ β π½) β (πΉ β π§) β (KQβπ½)) |
15 | 11, 12, 14 | syl2anc 584 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (πΉ β π§) β (KQβπ½)) |
16 | | toponuni 22407 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
17 | 11, 16 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π = βͺ π½) |
18 | 17 | difeq1d 4120 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π β ((clsβπ½)βπ§)) = (βͺ π½ β ((clsβπ½)βπ§))) |
19 | | topontop 22406 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β π½ β Top) |
20 | 11, 19 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π½ β Top) |
21 | | elssuni 4940 |
. . . . . . . . . . 11
β’ (π§ β π½ β π§ β βͺ π½) |
22 | 12, 21 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π§ β βͺ π½) |
23 | | eqid 2732 |
. . . . . . . . . . 11
β’ βͺ π½ =
βͺ π½ |
24 | 23 | clscld 22542 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π§ β βͺ π½)
β ((clsβπ½)βπ§) β (Clsdβπ½)) |
25 | 20, 22, 24 | syl2anc 584 |
. . . . . . . . 9
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β ((clsβπ½)βπ§) β (Clsdβπ½)) |
26 | 23 | cldopn 22526 |
. . . . . . . . 9
β’
(((clsβπ½)βπ§) β (Clsdβπ½) β (βͺ π½ β ((clsβπ½)βπ§)) β π½) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (βͺ π½ β ((clsβπ½)βπ§)) β π½) |
28 | 18, 27 | eqeltrd 2833 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π β ((clsβπ½)βπ§)) β π½) |
29 | 13 | kqopn 23229 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ (π β ((clsβπ½)βπ§)) β π½) β (πΉ β (π β ((clsβπ½)βπ§))) β (KQβπ½)) |
30 | 11, 28, 29 | syl2anc 584 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (πΉ β (π β ((clsβπ½)βπ§))) β (KQβπ½)) |
31 | | simprrl 779 |
. . . . . . . 8
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β π΄ β π§) |
32 | 31 | adantr 481 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π΄ β π§) |
33 | | regr1lem.4 |
. . . . . . . . 9
β’ (π β π΄ β π) |
34 | 33 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π΄ β π) |
35 | 13 | kqfvima 23225 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π§ β π½ β§ π΄ β π) β (π΄ β π§ β (πΉβπ΄) β (πΉ β π§))) |
36 | 11, 12, 34, 35 | syl3anc 1371 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π΄ β π§ β (πΉβπ΄) β (πΉ β π§))) |
37 | 32, 36 | mpbid 231 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (πΉβπ΄) β (πΉ β π§)) |
38 | | regr1lem.5 |
. . . . . . . . 9
β’ (π β π΅ β π) |
39 | 38 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π΅ β π) |
40 | | simprrr 780 |
. . . . . . . . . 10
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β ((clsβπ½)βπ§) β π) |
41 | 40 | sseld 3980 |
. . . . . . . . 9
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β (π΅ β ((clsβπ½)βπ§) β π΅ β π)) |
42 | 41 | con3dimp 409 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β Β¬ π΅ β ((clsβπ½)βπ§)) |
43 | 39, 42 | eldifd 3958 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π΅ β (π β ((clsβπ½)βπ§))) |
44 | 13 | kqfvima 23225 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ (π β ((clsβπ½)βπ§)) β π½ β§ π΅ β π) β (π΅ β (π β ((clsβπ½)βπ§)) β (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))))) |
45 | 11, 28, 39, 44 | syl3anc 1371 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π΅ β (π β ((clsβπ½)βπ§)) β (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))))) |
46 | 43, 45 | mpbid 231 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§)))) |
47 | 23 | sscls 22551 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π§ β βͺ π½)
β π§ β
((clsβπ½)βπ§)) |
48 | 20, 22, 47 | syl2anc 584 |
. . . . . . . . 9
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π§ β ((clsβπ½)βπ§)) |
49 | 48 | sscond 4140 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π β ((clsβπ½)βπ§)) β (π β π§)) |
50 | | imass2 6098 |
. . . . . . . 8
β’ ((π β ((clsβπ½)βπ§)) β (π β π§) β (πΉ β (π β ((clsβπ½)βπ§))) β (πΉ β (π β π§))) |
51 | | sslin 4233 |
. . . . . . . 8
β’ ((πΉ β (π β ((clsβπ½)βπ§))) β (πΉ β (π β π§)) β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) β ((πΉ β π§) β© (πΉ β (π β π§)))) |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) β ((πΉ β π§) β© (πΉ β (π β π§)))) |
53 | 13 | kqdisj 23227 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π§ β π½) β ((πΉ β π§) β© (πΉ β (π β π§))) = β
) |
54 | 11, 12, 53 | syl2anc 584 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β ((πΉ β π§) β© (πΉ β (π β π§))) = β
) |
55 | | sseq0 4398 |
. . . . . . 7
β’ ((((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) β ((πΉ β π§) β© (πΉ β (π β π§))) β§ ((πΉ β π§) β© (πΉ β (π β π§))) = β
) β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
) |
56 | 52, 54, 55 | syl2anc 584 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
) |
57 | | eleq2 2822 |
. . . . . . . 8
β’ (π = (πΉ β π§) β ((πΉβπ΄) β π β (πΉβπ΄) β (πΉ β π§))) |
58 | | ineq1 4204 |
. . . . . . . . 9
β’ (π = (πΉ β π§) β (π β© π) = ((πΉ β π§) β© π)) |
59 | 58 | eqeq1d 2734 |
. . . . . . . 8
β’ (π = (πΉ β π§) β ((π β© π) = β
β ((πΉ β π§) β© π) = β
)) |
60 | 57, 59 | 3anbi13d 1438 |
. . . . . . 7
β’ (π = (πΉ β π§) β (((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
) β ((πΉβπ΄) β (πΉ β π§) β§ (πΉβπ΅) β π β§ ((πΉ β π§) β© π) = β
))) |
61 | | eleq2 2822 |
. . . . . . . 8
β’ (π = (πΉ β (π β ((clsβπ½)βπ§))) β ((πΉβπ΅) β π β (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))))) |
62 | | ineq2 4205 |
. . . . . . . . 9
β’ (π = (πΉ β (π β ((clsβπ½)βπ§))) β ((πΉ β π§) β© π) = ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§))))) |
63 | 62 | eqeq1d 2734 |
. . . . . . . 8
β’ (π = (πΉ β (π β ((clsβπ½)βπ§))) β (((πΉ β π§) β© π) = β
β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
)) |
64 | 61, 63 | 3anbi23d 1439 |
. . . . . . 7
β’ (π = (πΉ β (π β ((clsβπ½)βπ§))) β (((πΉβπ΄) β (πΉ β π§) β§ (πΉβπ΅) β π β§ ((πΉ β π§) β© π) = β
) β ((πΉβπ΄) β (πΉ β π§) β§ (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))) β§ ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
))) |
65 | 60, 64 | rspc2ev 3623 |
. . . . . 6
β’ (((πΉ β π§) β (KQβπ½) β§ (πΉ β (π β ((clsβπ½)βπ§))) β (KQβπ½) β§ ((πΉβπ΄) β (πΉ β π§) β§ (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))) β§ ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
)) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
)) |
66 | 15, 30, 37, 46, 56, 65 | syl113anc 1382 |
. . . . 5
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
)) |
67 | 66 | ex 413 |
. . . 4
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β (Β¬ π΅ β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
))) |
68 | 9, 67 | mt3d 148 |
. . 3
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β π΅ β π) |
69 | 7, 68 | rexlimddv 3161 |
. 2
β’ ((π β§ π΄ β π) β π΅ β π) |
70 | 69 | ex 413 |
1
β’ (π β (π΄ β π β π΅ β π)) |