Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . . . . 10
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
2 | | simplll 774 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π½ β (TopOnβπ)) |
3 | | simpllr 775 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π½ β Reg) |
4 | | simplrl 776 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π§ β π) |
5 | | simplrr 777 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π€ β π) |
6 | | simprl 770 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π β π½) |
7 | | simprr 772 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)) |
8 | 1, 2, 3, 4, 5, 6, 7 | regr1lem 23243 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β (π§ β π β π€ β π)) |
9 | | 3ancoma 1099 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β ((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
10 | | incom 4202 |
. . . . . . . . . . . . . . . 16
β’ (π β© π) = (π β© π) |
11 | 10 | eqeq1i 2738 |
. . . . . . . . . . . . . . 15
β’ ((π β© π) = β
β (π β© π) = β
) |
12 | 11 | 3anbi3i 1160 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
) β ((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
13 | 9, 12 | bitri 275 |
. . . . . . . . . . . . 13
β’ (((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β ((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
14 | 13 | 2rexbii 3130 |
. . . . . . . . . . . 12
β’
(βπ β
(KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
15 | | rexcom 3288 |
. . . . . . . . . . . 12
β’
(βπ β
(KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
16 | 14, 15 | bitri 275 |
. . . . . . . . . . 11
β’
(βπ β
(KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
17 | 7, 16 | sylnib 328 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
18 | 1, 2, 3, 5, 4, 6, 17 | regr1lem 23243 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β (π€ β π β π§ β π)) |
19 | 8, 18 | impbid 211 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β (π§ β π β π€ β π)) |
20 | 19 | expr 458 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ π β π½) β (Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β (π§ β π β π€ β π))) |
21 | 20 | ralrimdva 3155 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β (Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β βπ β π½ (π§ β π β π€ β π))) |
22 | 1 | kqfeq 23228 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π€ β π) β ((πΉβπ§) = (πΉβπ€) β βπ¦ β π½ (π§ β π¦ β π€ β π¦))) |
23 | | elequ2 2122 |
. . . . . . . . . . 11
β’ (π¦ = π β (π§ β π¦ β π§ β π)) |
24 | | elequ2 2122 |
. . . . . . . . . . 11
β’ (π¦ = π β (π€ β π¦ β π€ β π)) |
25 | 23, 24 | bibi12d 346 |
. . . . . . . . . 10
β’ (π¦ = π β ((π§ β π¦ β π€ β π¦) β (π§ β π β π€ β π))) |
26 | 25 | cbvralvw 3235 |
. . . . . . . . 9
β’
(βπ¦ β
π½ (π§ β π¦ β π€ β π¦) β βπ β π½ (π§ β π β π€ β π)) |
27 | 22, 26 | bitrdi 287 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π€ β π) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
28 | 27 | 3expb 1121 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ (π§ β π β§ π€ β π)) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
29 | 28 | adantlr 714 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
30 | 21, 29 | sylibrd 259 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β (Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β (πΉβπ§) = (πΉβπ€))) |
31 | 30 | necon1ad 2958 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) |
32 | 31 | ralrimivva 3201 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β βπ§ β π βπ€ β π ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) |
33 | 1 | kqffn 23229 |
. . . . 5
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
34 | 33 | adantr 482 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β πΉ Fn π) |
35 | | neeq1 3004 |
. . . . . . . 8
β’ (π = (πΉβπ§) β (π β π β (πΉβπ§) β π)) |
36 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = (πΉβπ§) β (π β π β (πΉβπ§) β π)) |
37 | 36 | 3anbi1d 1441 |
. . . . . . . . 9
β’ (π = (πΉβπ§) β ((π β π β§ π β π β§ (π β© π) = β
) β ((πΉβπ§) β π β§ π β π β§ (π β© π) = β
))) |
38 | 37 | 2rexbidv 3220 |
. . . . . . . 8
β’ (π = (πΉβπ§) β (βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
))) |
39 | 35, 38 | imbi12d 345 |
. . . . . . 7
β’ (π = (πΉβπ§) β ((π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)) β ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)))) |
40 | 39 | ralbidv 3178 |
. . . . . 6
β’ (π = (πΉβπ§) β (βπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)) β βπ β ran πΉ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)))) |
41 | 40 | ralrn 7090 |
. . . . 5
β’ (πΉ Fn π β (βπ β ran πΉβπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)) β βπ§ β π βπ β ran πΉ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)))) |
42 | | neeq2 3005 |
. . . . . . . 8
β’ (π = (πΉβπ€) β ((πΉβπ§) β π β (πΉβπ§) β (πΉβπ€))) |
43 | | eleq1 2822 |
. . . . . . . . . 10
β’ (π = (πΉβπ€) β (π β π β (πΉβπ€) β π)) |
44 | 43 | 3anbi2d 1442 |
. . . . . . . . 9
β’ (π = (πΉβπ€) β (((πΉβπ§) β π β§ π β π β§ (π β© π) = β
) β ((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) |
45 | 44 | 2rexbidv 3220 |
. . . . . . . 8
β’ (π = (πΉβπ€) β (βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) |
46 | 42, 45 | imbi12d 345 |
. . . . . . 7
β’ (π = (πΉβπ€) β (((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)) β ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)))) |
47 | 46 | ralrn 7090 |
. . . . . 6
β’ (πΉ Fn π β (βπ β ran πΉ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)) β βπ€ β π ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)))) |
48 | 47 | ralbidv 3178 |
. . . . 5
β’ (πΉ Fn π β (βπ§ β π βπ β ran πΉ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)) β βπ§ β π βπ€ β π ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)))) |
49 | 41, 48 | bitrd 279 |
. . . 4
β’ (πΉ Fn π β (βπ β ran πΉβπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)) β βπ§ β π βπ€ β π ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)))) |
50 | 34, 49 | syl 17 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (βπ β ran πΉβπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)) β βπ§ β π βπ€ β π ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)))) |
51 | 32, 50 | mpbird 257 |
. 2
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β βπ β ran πΉβπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
))) |
52 | 1 | kqtopon 23231 |
. . . 4
β’ (π½ β (TopOnβπ) β (KQβπ½) β (TopOnβran πΉ)) |
53 | 52 | adantr 482 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (KQβπ½) β (TopOnβran πΉ)) |
54 | | ishaus2 22855 |
. . 3
β’
((KQβπ½) β
(TopOnβran πΉ) β
((KQβπ½) β Haus
β βπ β ran
πΉβπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)))) |
55 | 53, 54 | syl 17 |
. 2
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β ((KQβπ½) β Haus β
βπ β ran πΉβπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)))) |
56 | 51, 55 | mpbird 257 |
1
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (KQβπ½) β Haus) |