Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . 5
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
2 | 1 | kqtopon 23081 |
. . . 4
β’ (π½ β (TopOnβπ) β (KQβπ½) β (TopOnβran πΉ)) |
3 | 2 | adantr 482 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (KQβπ½) β (TopOnβran πΉ)) |
4 | | topontop 22265 |
. . 3
β’
((KQβπ½) β
(TopOnβran πΉ) β
(KQβπ½) β
Top) |
5 | 3, 4 | syl 17 |
. 2
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (KQβπ½) β Top) |
6 | | toponss 22279 |
. . . . . . . 8
β’
(((KQβπ½)
β (TopOnβran πΉ)
β§ π β
(KQβπ½)) β π β ran πΉ) |
7 | 3, 6 | sylan 581 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β π β ran πΉ) |
8 | 7 | sselda 3945 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π β π) β π β ran πΉ) |
9 | 1 | kqffn 23079 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
10 | 9 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π β π) β πΉ Fn π) |
11 | | fvelrnb 6904 |
. . . . . . 7
β’ (πΉ Fn π β (π β ran πΉ β βπ§ β π (πΉβπ§) = π)) |
12 | 10, 11 | syl 17 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π β π) β (π β ran πΉ β βπ§ β π (πΉβπ§) = π)) |
13 | 8, 12 | mpbid 231 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π β π) β βπ§ β π (πΉβπ§) = π) |
14 | | simpllr 775 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β π½ β Reg) |
15 | 1 | kqid 23082 |
. . . . . . . . . . . . . . 15
β’ (π½ β (TopOnβπ) β πΉ β (π½ Cn (KQβπ½))) |
16 | 15 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β πΉ β (π½ Cn (KQβπ½))) |
17 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β π β (KQβπ½)) |
18 | | cnima 22619 |
. . . . . . . . . . . . . 14
β’ ((πΉ β (π½ Cn (KQβπ½)) β§ π β (KQβπ½)) β (β‘πΉ β π) β π½) |
19 | 16, 17, 18 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β (β‘πΉ β π) β π½) |
20 | 9 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β πΉ Fn π) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β πΉ Fn π) |
22 | | elpreima 7009 |
. . . . . . . . . . . . . . 15
β’ (πΉ Fn π β (π§ β (β‘πΉ β π) β (π§ β π β§ (πΉβπ§) β π))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β (π§ β (β‘πΉ β π) β (π§ β π β§ (πΉβπ§) β π))) |
24 | 23 | biimpar 479 |
. . . . . . . . . . . . 13
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β π§ β (β‘πΉ β π)) |
25 | | regsep 22688 |
. . . . . . . . . . . . 13
β’ ((π½ β Reg β§ (β‘πΉ β π) β π½ β§ π§ β (β‘πΉ β π)) β βπ€ β π½ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π))) |
26 | 14, 19, 24, 25 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β βπ€ β π½ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π))) |
27 | | simp-4l 782 |
. . . . . . . . . . . . . 14
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β π½ β (TopOnβπ)) |
28 | | simprl 770 |
. . . . . . . . . . . . . 14
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β π€ β π½) |
29 | 1 | kqopn 23088 |
. . . . . . . . . . . . . 14
β’ ((π½ β (TopOnβπ) β§ π€ β π½) β (πΉ β π€) β (KQβπ½)) |
30 | 27, 28, 29 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β (πΉ β π€) β (KQβπ½)) |
31 | | simprrl 780 |
. . . . . . . . . . . . . 14
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β π§ β π€) |
32 | | simplrl 776 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β π§ β π) |
33 | 1 | kqfvima 23084 |
. . . . . . . . . . . . . . 15
β’ ((π½ β (TopOnβπ) β§ π€ β π½ β§ π§ β π) β (π§ β π€ β (πΉβπ§) β (πΉ β π€))) |
34 | 27, 28, 32, 33 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β (π§ β π€ β (πΉβπ§) β (πΉ β π€))) |
35 | 31, 34 | mpbid 231 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β (πΉβπ§) β (πΉ β π€)) |
36 | | topontop 22265 |
. . . . . . . . . . . . . . . . . 18
β’ (π½ β (TopOnβπ) β π½ β Top) |
37 | 27, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β π½ β Top) |
38 | | elssuni 4899 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β π½ β π€ β βͺ π½) |
39 | 38 | ad2antrl 727 |
. . . . . . . . . . . . . . . . 17
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β π€ β βͺ π½) |
40 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π½ =
βͺ π½ |
41 | 40 | clscld 22401 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ π€ β βͺ π½)
β ((clsβπ½)βπ€) β (Clsdβπ½)) |
42 | 37, 39, 41 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β ((clsβπ½)βπ€) β (Clsdβπ½)) |
43 | 1 | kqcld 23089 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (TopOnβπ) β§ ((clsβπ½)βπ€) β (Clsdβπ½)) β (πΉ β ((clsβπ½)βπ€)) β (Clsdβ(KQβπ½))) |
44 | 27, 42, 43 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β (πΉ β ((clsβπ½)βπ€)) β (Clsdβ(KQβπ½))) |
45 | 40 | sscls 22410 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ π€ β βͺ π½)
β π€ β
((clsβπ½)βπ€)) |
46 | 37, 39, 45 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β π€ β ((clsβπ½)βπ€)) |
47 | | imass2 6055 |
. . . . . . . . . . . . . . . 16
β’ (π€ β ((clsβπ½)βπ€) β (πΉ β π€) β (πΉ β ((clsβπ½)βπ€))) |
48 | 46, 47 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β (πΉ β π€) β (πΉ β ((clsβπ½)βπ€))) |
49 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ βͺ (KQβπ½) = βͺ
(KQβπ½) |
50 | 49 | clsss2 22426 |
. . . . . . . . . . . . . . 15
β’ (((πΉ β ((clsβπ½)βπ€)) β (Clsdβ(KQβπ½)) β§ (πΉ β π€) β (πΉ β ((clsβπ½)βπ€))) β ((clsβ(KQβπ½))β(πΉ β π€)) β (πΉ β ((clsβπ½)βπ€))) |
51 | 44, 48, 50 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β ((clsβ(KQβπ½))β(πΉ β π€)) β (πΉ β ((clsβπ½)βπ€))) |
52 | 20 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β πΉ Fn π) |
53 | | fnfun 6603 |
. . . . . . . . . . . . . . . 16
β’ (πΉ Fn π β Fun πΉ) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β Fun πΉ) |
55 | | simprrr 781 |
. . . . . . . . . . . . . . 15
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β ((clsβπ½)βπ€) β (β‘πΉ β π)) |
56 | | funimass2 6585 |
. . . . . . . . . . . . . . 15
β’ ((Fun
πΉ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)) β (πΉ β ((clsβπ½)βπ€)) β π) |
57 | 54, 55, 56 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β (πΉ β ((clsβπ½)βπ€)) β π) |
58 | 51, 57 | sstrd 3955 |
. . . . . . . . . . . . 13
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β ((clsβ(KQβπ½))β(πΉ β π€)) β π) |
59 | | eleq2 2827 |
. . . . . . . . . . . . . . 15
β’ (π = (πΉ β π€) β ((πΉβπ§) β π β (πΉβπ§) β (πΉ β π€))) |
60 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π = (πΉ β π€) β ((clsβ(KQβπ½))βπ) = ((clsβ(KQβπ½))β(πΉ β π€))) |
61 | 60 | sseq1d 3976 |
. . . . . . . . . . . . . . 15
β’ (π = (πΉ β π€) β (((clsβ(KQβπ½))βπ) β π β ((clsβ(KQβπ½))β(πΉ β π€)) β π)) |
62 | 59, 61 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π = (πΉ β π€) β (((πΉβπ§) β π β§ ((clsβ(KQβπ½))βπ) β π) β ((πΉβπ§) β (πΉ β π€) β§ ((clsβ(KQβπ½))β(πΉ β π€)) β π))) |
63 | 62 | rspcev 3582 |
. . . . . . . . . . . . 13
β’ (((πΉ β π€) β (KQβπ½) β§ ((πΉβπ§) β (πΉ β π€) β§ ((clsβ(KQβπ½))β(πΉ β π€)) β π)) β βπ β (KQβπ½)((πΉβπ§) β π β§ ((clsβ(KQβπ½))βπ) β π)) |
64 | 30, 35, 58, 63 | syl12anc 836 |
. . . . . . . . . . . 12
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β§ (π€ β π½ β§ (π§ β π€ β§ ((clsβπ½)βπ€) β (β‘πΉ β π)))) β βπ β (KQβπ½)((πΉβπ§) β π β§ ((clsβ(KQβπ½))βπ) β π)) |
65 | 26, 64 | rexlimddv 3159 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ (π§ β π β§ (πΉβπ§) β π)) β βπ β (KQβπ½)((πΉβπ§) β π β§ ((clsβ(KQβπ½))βπ) β π)) |
66 | 65 | expr 458 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π§ β π) β ((πΉβπ§) β π β βπ β (KQβπ½)((πΉβπ§) β π β§ ((clsβ(KQβπ½))βπ) β π))) |
67 | | eleq1 2826 |
. . . . . . . . . . 11
β’ ((πΉβπ§) = π β ((πΉβπ§) β π β π β π)) |
68 | | eleq1 2826 |
. . . . . . . . . . . . 13
β’ ((πΉβπ§) = π β ((πΉβπ§) β π β π β π)) |
69 | 68 | anbi1d 631 |
. . . . . . . . . . . 12
β’ ((πΉβπ§) = π β (((πΉβπ§) β π β§ ((clsβ(KQβπ½))βπ) β π) β (π β π β§ ((clsβ(KQβπ½))βπ) β π))) |
70 | 69 | rexbidv 3176 |
. . . . . . . . . . 11
β’ ((πΉβπ§) = π β (βπ β (KQβπ½)((πΉβπ§) β π β§ ((clsβ(KQβπ½))βπ) β π) β βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π))) |
71 | 67, 70 | imbi12d 345 |
. . . . . . . . . 10
β’ ((πΉβπ§) = π β (((πΉβπ§) β π β βπ β (KQβπ½)((πΉβπ§) β π β§ ((clsβ(KQβπ½))βπ) β π)) β (π β π β βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π)))) |
72 | 66, 71 | syl5ibcom 244 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π§ β π) β ((πΉβπ§) = π β (π β π β βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π)))) |
73 | 72 | com23 86 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π§ β π) β (π β π β ((πΉβπ§) = π β βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π)))) |
74 | 73 | imp 408 |
. . . . . . 7
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π§ β π) β§ π β π) β ((πΉβπ§) = π β βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π))) |
75 | 74 | an32s 651 |
. . . . . 6
β’
(((((π½ β
(TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π β π) β§ π§ β π) β ((πΉβπ§) = π β βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π))) |
76 | 75 | rexlimdva 3153 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π β π) β (βπ§ β π (πΉβπ§) = π β βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π))) |
77 | 13, 76 | mpd 15 |
. . . 4
β’ ((((π½ β (TopOnβπ) β§ π½ β Reg) β§ π β (KQβπ½)) β§ π β π) β βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π)) |
78 | 77 | anasss 468 |
. . 3
β’ (((π½ β (TopOnβπ) β§ π½ β Reg) β§ (π β (KQβπ½) β§ π β π)) β βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π)) |
79 | 78 | ralrimivva 3198 |
. 2
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β βπ β (KQβπ½)βπ β π βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π)) |
80 | | isreg 22686 |
. 2
β’
((KQβπ½) β
Reg β ((KQβπ½)
β Top β§ βπ
β (KQβπ½)βπ β π βπ β (KQβπ½)(π β π β§ ((clsβ(KQβπ½))βπ) β π))) |
81 | 5, 79, 80 | sylanbrc 584 |
1
β’ ((π½ β (TopOnβπ) β§ π½ β Reg) β (KQβπ½) β Reg) |