Step | Hyp | Ref
| Expression |
1 | | regr1lem.3 |
. . . . 5
β’ (π β π½ β Reg) |
2 | 1 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β π) β π½ β Reg) |
3 | | regr1lem.6 |
. . . . 5
β’ (π β π β π½) |
4 | 3 | adantr 482 |
. . . 4
β’ ((π β§ π΄ β π) β π β π½) |
5 | | simpr 486 |
. . . 4
β’ ((π β§ π΄ β π) β π΄ β π) |
6 | | regsep 22701 |
. . . 4
β’ ((π½ β Reg β§ π β π½ β§ π΄ β π) β βπ§ β π½ (π΄ β π§ β§ ((clsβπ½)βπ§) β π)) |
7 | 2, 4, 5, 6 | syl3anc 1372 |
. . 3
β’ ((π β§ π΄ β π) β βπ§ β π½ (π΄ β π§ β§ ((clsβπ½)βπ§) β π)) |
8 | | regr1lem.7 |
. . . . 5
β’ (π β Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
)) |
9 | 8 | ad2antrr 725 |
. . . 4
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
)) |
10 | | regr1lem.2 |
. . . . . . . 8
β’ (π β π½ β (TopOnβπ)) |
11 | 10 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π½ β (TopOnβπ)) |
12 | | simplrl 776 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π§ β π½) |
13 | | kqval.2 |
. . . . . . . 8
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
14 | 13 | kqopn 23101 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π§ β π½) β (πΉ β π§) β (KQβπ½)) |
15 | 11, 12, 14 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (πΉ β π§) β (KQβπ½)) |
16 | | toponuni 22279 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
17 | 11, 16 | syl 17 |
. . . . . . . . 9
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π = βͺ π½) |
18 | 17 | difeq1d 4086 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π β ((clsβπ½)βπ§)) = (βͺ π½ β ((clsβπ½)βπ§))) |
19 | | topontop 22278 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β π½ β Top) |
20 | 11, 19 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π½ β Top) |
21 | | elssuni 4903 |
. . . . . . . . . . 11
β’ (π§ β π½ β π§ β βͺ π½) |
22 | 12, 21 | syl 17 |
. . . . . . . . . 10
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π§ β βͺ π½) |
23 | | eqid 2737 |
. . . . . . . . . . 11
β’ βͺ π½ =
βͺ π½ |
24 | 23 | clscld 22414 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π§ β βͺ π½)
β ((clsβπ½)βπ§) β (Clsdβπ½)) |
25 | 20, 22, 24 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β ((clsβπ½)βπ§) β (Clsdβπ½)) |
26 | 23 | cldopn 22398 |
. . . . . . . . 9
β’
(((clsβπ½)βπ§) β (Clsdβπ½) β (βͺ π½ β ((clsβπ½)βπ§)) β π½) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (βͺ π½ β ((clsβπ½)βπ§)) β π½) |
28 | 18, 27 | eqeltrd 2838 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π β ((clsβπ½)βπ§)) β π½) |
29 | 13 | kqopn 23101 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ (π β ((clsβπ½)βπ§)) β π½) β (πΉ β (π β ((clsβπ½)βπ§))) β (KQβπ½)) |
30 | 11, 28, 29 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (πΉ β (π β ((clsβπ½)βπ§))) β (KQβπ½)) |
31 | | simprrl 780 |
. . . . . . . 8
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β π΄ β π§) |
32 | 31 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π΄ β π§) |
33 | | regr1lem.4 |
. . . . . . . . 9
β’ (π β π΄ β π) |
34 | 33 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π΄ β π) |
35 | 13 | kqfvima 23097 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π§ β π½ β§ π΄ β π) β (π΄ β π§ β (πΉβπ΄) β (πΉ β π§))) |
36 | 11, 12, 34, 35 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π΄ β π§ β (πΉβπ΄) β (πΉ β π§))) |
37 | 32, 36 | mpbid 231 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (πΉβπ΄) β (πΉ β π§)) |
38 | | regr1lem.5 |
. . . . . . . . 9
β’ (π β π΅ β π) |
39 | 38 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π΅ β π) |
40 | | simprrr 781 |
. . . . . . . . . 10
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β ((clsβπ½)βπ§) β π) |
41 | 40 | sseld 3948 |
. . . . . . . . 9
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β (π΅ β ((clsβπ½)βπ§) β π΅ β π)) |
42 | 41 | con3dimp 410 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β Β¬ π΅ β ((clsβπ½)βπ§)) |
43 | 39, 42 | eldifd 3926 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π΅ β (π β ((clsβπ½)βπ§))) |
44 | 13 | kqfvima 23097 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ (π β ((clsβπ½)βπ§)) β π½ β§ π΅ β π) β (π΅ β (π β ((clsβπ½)βπ§)) β (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))))) |
45 | 11, 28, 39, 44 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π΅ β (π β ((clsβπ½)βπ§)) β (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))))) |
46 | 43, 45 | mpbid 231 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§)))) |
47 | 23 | sscls 22423 |
. . . . . . . . . 10
β’ ((π½ β Top β§ π§ β βͺ π½)
β π§ β
((clsβπ½)βπ§)) |
48 | 20, 22, 47 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β π§ β ((clsβπ½)βπ§)) |
49 | 48 | sscond 4106 |
. . . . . . . 8
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β (π β ((clsβπ½)βπ§)) β (π β π§)) |
50 | | imass2 6059 |
. . . . . . . 8
β’ ((π β ((clsβπ½)βπ§)) β (π β π§) β (πΉ β (π β ((clsβπ½)βπ§))) β (πΉ β (π β π§))) |
51 | | sslin 4199 |
. . . . . . . 8
β’ ((πΉ β (π β ((clsβπ½)βπ§))) β (πΉ β (π β π§)) β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) β ((πΉ β π§) β© (πΉ β (π β π§)))) |
52 | 49, 50, 51 | 3syl 18 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) β ((πΉ β π§) β© (πΉ β (π β π§)))) |
53 | 13 | kqdisj 23099 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π§ β π½) β ((πΉ β π§) β© (πΉ β (π β π§))) = β
) |
54 | 11, 12, 53 | syl2anc 585 |
. . . . . . 7
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β ((πΉ β π§) β© (πΉ β (π β π§))) = β
) |
55 | | sseq0 4364 |
. . . . . . 7
β’ ((((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) β ((πΉ β π§) β© (πΉ β (π β π§))) β§ ((πΉ β π§) β© (πΉ β (π β π§))) = β
) β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
) |
56 | 52, 54, 55 | syl2anc 585 |
. . . . . 6
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
) |
57 | | eleq2 2827 |
. . . . . . . 8
β’ (π = (πΉ β π§) β ((πΉβπ΄) β π β (πΉβπ΄) β (πΉ β π§))) |
58 | | ineq1 4170 |
. . . . . . . . 9
β’ (π = (πΉ β π§) β (π β© π) = ((πΉ β π§) β© π)) |
59 | 58 | eqeq1d 2739 |
. . . . . . . 8
β’ (π = (πΉ β π§) β ((π β© π) = β
β ((πΉ β π§) β© π) = β
)) |
60 | 57, 59 | 3anbi13d 1439 |
. . . . . . 7
β’ (π = (πΉ β π§) β (((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
) β ((πΉβπ΄) β (πΉ β π§) β§ (πΉβπ΅) β π β§ ((πΉ β π§) β© π) = β
))) |
61 | | eleq2 2827 |
. . . . . . . 8
β’ (π = (πΉ β (π β ((clsβπ½)βπ§))) β ((πΉβπ΅) β π β (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))))) |
62 | | ineq2 4171 |
. . . . . . . . 9
β’ (π = (πΉ β (π β ((clsβπ½)βπ§))) β ((πΉ β π§) β© π) = ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§))))) |
63 | 62 | eqeq1d 2739 |
. . . . . . . 8
β’ (π = (πΉ β (π β ((clsβπ½)βπ§))) β (((πΉ β π§) β© π) = β
β ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
)) |
64 | 61, 63 | 3anbi23d 1440 |
. . . . . . 7
β’ (π = (πΉ β (π β ((clsβπ½)βπ§))) β (((πΉβπ΄) β (πΉ β π§) β§ (πΉβπ΅) β π β§ ((πΉ β π§) β© π) = β
) β ((πΉβπ΄) β (πΉ β π§) β§ (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))) β§ ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
))) |
65 | 60, 64 | rspc2ev 3595 |
. . . . . 6
β’ (((πΉ β π§) β (KQβπ½) β§ (πΉ β (π β ((clsβπ½)βπ§))) β (KQβπ½) β§ ((πΉβπ΄) β (πΉ β π§) β§ (πΉβπ΅) β (πΉ β (π β ((clsβπ½)βπ§))) β§ ((πΉ β π§) β© (πΉ β (π β ((clsβπ½)βπ§)))) = β
)) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
)) |
66 | 15, 30, 37, 46, 56, 65 | syl113anc 1383 |
. . . . 5
β’ ((((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β§ Β¬ π΅ β π) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
)) |
67 | 66 | ex 414 |
. . . 4
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β (Β¬ π΅ β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ΄) β π β§ (πΉβπ΅) β π β§ (π β© π) = β
))) |
68 | 9, 67 | mt3d 148 |
. . 3
β’ (((π β§ π΄ β π) β§ (π§ β π½ β§ (π΄ β π§ β§ ((clsβπ½)βπ§) β π))) β π΅ β π) |
69 | 7, 68 | rexlimddv 3159 |
. 2
β’ ((π β§ π΄ β π) β π΅ β π) |
70 | 69 | ex 414 |
1
β’ (π β (π΄ β π β π΅ β π)) |