Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . . . . 10
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
2 | | simplll 771 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π½ β (TopOnβπ)) |
3 | | simpllr 772 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π½ β Reg) |
4 | | simplrl 773 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π§ β π) |
5 | | simplrr 774 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π€ β π) |
6 | | simprl 767 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β π β π½) |
7 | | simprr 769 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)) |
8 | 1, 2, 3, 4, 5, 6, 7 | regr1lem 23463 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β (π§ β π β π€ β π)) |
9 | | 3ancoma 1096 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β ((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
10 | | incom 4200 |
. . . . . . . . . . . . . . . 16
β’ (π β© π) = (π β© π) |
11 | 10 | eqeq1i 2735 |
. . . . . . . . . . . . . . 15
β’ ((π β© π) = β
β (π β© π) = β
) |
12 | 11 | 3anbi3i 1157 |
. . . . . . . . . . . . . 14
β’ (((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
) β ((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
13 | 9, 12 | bitri 274 |
. . . . . . . . . . . . 13
β’ (((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β ((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
14 | 13 | 2rexbii 3127 |
. . . . . . . . . . . 12
β’
(βπ β
(KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
15 | | rexcom 3285 |
. . . . . . . . . . . 12
β’
(βπ β
(KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
16 | 14, 15 | bitri 274 |
. . . . . . . . . . 11
β’
(βπ β
(KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
17 | 7, 16 | sylnib 327 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ€) β π β§ (πΉβπ§) β π β§ (π β© π) = β
)) |
18 | 1, 2, 3, 5, 4, 6, 17 | regr1lem 23463 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β (π€ β π β π§ β π)) |
19 | 8, 18 | impbid 211 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ (π β π½ β§ Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) β (π§ β π β π€ β π)) |
20 | 19 | expr 455 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β§ π β π½) β (Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β (π§ β π β π€ β π))) |
21 | 20 | ralrimdva 3152 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β (Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β βπ β π½ (π§ β π β π€ β π))) |
22 | 1 | kqfeq 23448 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π€ β π) β ((πΉβπ§) = (πΉβπ€) β βπ¦ β π½ (π§ β π¦ β π€ β π¦))) |
23 | | elequ2 2119 |
. . . . . . . . . . 11
β’ (π¦ = π β (π§ β π¦ β π§ β π)) |
24 | | elequ2 2119 |
. . . . . . . . . . 11
β’ (π¦ = π β (π€ β π¦ β π€ β π)) |
25 | 23, 24 | bibi12d 344 |
. . . . . . . . . 10
β’ (π¦ = π β ((π§ β π¦ β π€ β π¦) β (π§ β π β π€ β π))) |
26 | 25 | cbvralvw 3232 |
. . . . . . . . 9
β’
(βπ¦ β
π½ (π§ β π¦ β π€ β π¦) β βπ β π½ (π§ β π β π€ β π)) |
27 | 22, 26 | bitrdi 286 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π€ β π) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
28 | 27 | 3expb 1118 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ (π§ β π β§ π€ β π)) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
29 | 28 | adantlr 711 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
30 | 21, 29 | sylibrd 258 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β (Β¬ βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
) β (πΉβπ§) = (πΉβπ€))) |
31 | 30 | necon1ad 2955 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π§ β π β§ π€ β π)) β ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) |
32 | 31 | ralrimivva 3198 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β βπ§ β π βπ€ β π ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) |
33 | 1 | kqffn 23449 |
. . . . 5
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
34 | 33 | adantr 479 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β πΉ Fn π) |
35 | | neeq1 3001 |
. . . . . . . 8
β’ (π = (πΉβπ§) β (π β π β (πΉβπ§) β π)) |
36 | | eleq1 2819 |
. . . . . . . . . 10
β’ (π = (πΉβπ§) β (π β π β (πΉβπ§) β π)) |
37 | 36 | 3anbi1d 1438 |
. . . . . . . . 9
β’ (π = (πΉβπ§) β ((π β π β§ π β π β§ (π β© π) = β
) β ((πΉβπ§) β π β§ π β π β§ (π β© π) = β
))) |
38 | 37 | 2rexbidv 3217 |
. . . . . . . 8
β’ (π = (πΉβπ§) β (βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
))) |
39 | 35, 38 | imbi12d 343 |
. . . . . . 7
β’ (π = (πΉβπ§) β ((π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)) β ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)))) |
40 | 39 | ralbidv 3175 |
. . . . . 6
β’ (π = (πΉβπ§) β (βπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)) β βπ β ran πΉ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)))) |
41 | 40 | ralrn 7088 |
. . . . 5
β’ (πΉ Fn π β (βπ β ran πΉβπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
)) β βπ§ β π βπ β ran πΉ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)))) |
42 | | neeq2 3002 |
. . . . . . . 8
β’ (π = (πΉβπ€) β ((πΉβπ§) β π β (πΉβπ§) β (πΉβπ€))) |
43 | | eleq1 2819 |
. . . . . . . . . 10
β’ (π = (πΉβπ€) β (π β π β (πΉβπ€) β π)) |
44 | 43 | 3anbi2d 1439 |
. . . . . . . . 9
β’ (π = (πΉβπ€) β (((πΉβπ§) β π β§ π β π β§ (π β© π) = β
) β ((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) |
45 | 44 | 2rexbidv 3217 |
. . . . . . . 8
β’ (π = (πΉβπ€) β (βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
))) |
46 | 42, 45 | imbi12d 343 |
. . . . . . 7
β’ (π = (πΉβπ€) β (((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)) β ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)))) |
47 | 46 | ralrn 7088 |
. . . . . 6
β’ (πΉ Fn π β (βπ β ran πΉ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)) β βπ€ β π ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)))) |
48 | 47 | ralbidv 3175 |
. . . . 5
β’ (πΉ Fn π β (βπ§ β π βπ β ran πΉ((πΉβπ§) β π β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ π β π β§ (π β© π) = β
)) β βπ§ β π βπ€ β π ((πΉβπ§) β (πΉβπ€) β βπ β (KQβπ½)βπ β (KQβπ½)((πΉβπ§) β π β§ (πΉβπ€) β π β§ (π β© π) = β
)))) |
49 | 41, 48 | bitrd 278 |
. . . 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 256 |
. 2
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β βπ β ran πΉβπ β ran πΉ(π β π β βπ β (KQβπ½)βπ β (KQβπ½)(π β π β§ π β π β§ (π β© π) = β
))) |
52 | 1 | kqtopon 23451 |
. . . 4
β’ (π½ β (TopOnβπ) β (KQβπ½) β (TopOnβran πΉ)) |
53 | 52 | adantr 479 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (KQβπ½) β (TopOnβran πΉ)) |
54 | | ishaus2 23075 |
. . 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 256 |
1
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (KQβπ½) β Haus) |