Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . . . . . . 12
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
2 | 1 | kqid 23079 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β πΉ β (π½ Cn (KQβπ½))) |
3 | 2 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β πΉ β (π½ Cn (KQβπ½))) |
4 | | cnima 22616 |
. . . . . . . . . 10
β’ ((πΉ β (π½ Cn (KQβπ½)) β§ π£ β (KQβπ½)) β (β‘πΉ β π£) β π½) |
5 | 3, 4 | sylan 580 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β (β‘πΉ β π£) β π½) |
6 | | eleq2 2826 |
. . . . . . . . . . 11
β’ (π = (β‘πΉ β π£) β (π§ β π β π§ β (β‘πΉ β π£))) |
7 | | eleq2 2826 |
. . . . . . . . . . 11
β’ (π = (β‘πΉ β π£) β (π€ β π β π€ β (β‘πΉ β π£))) |
8 | 6, 7 | imbi12d 344 |
. . . . . . . . . 10
β’ (π = (β‘πΉ β π£) β ((π§ β π β π€ β π) β (π§ β (β‘πΉ β π£) β π€ β (β‘πΉ β π£)))) |
9 | 8 | rspcv 3577 |
. . . . . . . . 9
β’ ((β‘πΉ β π£) β π½ β (βπ β π½ (π§ β π β π€ β π) β (π§ β (β‘πΉ β π£) β π€ β (β‘πΉ β π£)))) |
10 | 5, 9 | syl 17 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β (βπ β π½ (π§ β π β π€ β π) β (π§ β (β‘πΉ β π£) β π€ β (β‘πΉ β π£)))) |
11 | 1 | kqffn 23076 |
. . . . . . . . . . . . 13
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
12 | 11 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β πΉ Fn π) |
13 | 12 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β πΉ Fn π) |
14 | | fnfun 6602 |
. . . . . . . . . . 11
β’ (πΉ Fn π β Fun πΉ) |
15 | 13, 14 | syl 17 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β Fun πΉ) |
16 | | simprl 769 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β π§ β π) |
17 | 16 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β π§ β π) |
18 | 13 | fndmd 6607 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β dom πΉ = π) |
19 | 17, 18 | eleqtrrd 2840 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β π§ β dom πΉ) |
20 | | fvimacnv 7003 |
. . . . . . . . . 10
β’ ((Fun
πΉ β§ π§ β dom πΉ) β ((πΉβπ§) β π£ β π§ β (β‘πΉ β π£))) |
21 | 15, 19, 20 | syl2anc 584 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β ((πΉβπ§) β π£ β π§ β (β‘πΉ β π£))) |
22 | | simprr 771 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β π€ β π) |
23 | 22 | adantr 481 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β π€ β π) |
24 | 23, 18 | eleqtrrd 2840 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β π€ β dom πΉ) |
25 | | fvimacnv 7003 |
. . . . . . . . . 10
β’ ((Fun
πΉ β§ π€ β dom πΉ) β ((πΉβπ€) β π£ β π€ β (β‘πΉ β π£))) |
26 | 15, 24, 25 | syl2anc 584 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β ((πΉβπ€) β π£ β π€ β (β‘πΉ β π£))) |
27 | 21, 26 | imbi12d 344 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β (((πΉβπ§) β π£ β (πΉβπ€) β π£) β (π§ β (β‘πΉ β π£) β π€ β (β‘πΉ β π£)))) |
28 | 10, 27 | sylibrd 258 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β§ π£ β (KQβπ½)) β (βπ β π½ (π§ β π β π€ β π) β ((πΉβπ§) β π£ β (πΉβπ€) β π£))) |
29 | 28 | ralrimdva 3151 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (βπ β π½ (π§ β π β π€ β π) β βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£))) |
30 | | simplr 767 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (KQβπ½) β Fre) |
31 | | fnfvelrn 7031 |
. . . . . . . . 9
β’ ((πΉ Fn π β§ π§ β π) β (πΉβπ§) β ran πΉ) |
32 | 12, 16, 31 | syl2anc 584 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (πΉβπ§) β ran πΉ) |
33 | 1 | kqtopon 23078 |
. . . . . . . . . 10
β’ (π½ β (TopOnβπ) β (KQβπ½) β (TopOnβran πΉ)) |
34 | 33 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (KQβπ½) β (TopOnβran πΉ)) |
35 | | toponuni 22263 |
. . . . . . . . 9
β’
((KQβπ½) β
(TopOnβran πΉ) β
ran πΉ = βͺ (KQβπ½)) |
36 | 34, 35 | syl 17 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β ran πΉ = βͺ
(KQβπ½)) |
37 | 32, 36 | eleqtrd 2839 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (πΉβπ§) β βͺ
(KQβπ½)) |
38 | | fnfvelrn 7031 |
. . . . . . . . 9
β’ ((πΉ Fn π β§ π€ β π) β (πΉβπ€) β ran πΉ) |
39 | 12, 22, 38 | syl2anc 584 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β ran πΉ) |
40 | 39, 36 | eleqtrd 2839 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (πΉβπ€) β βͺ
(KQβπ½)) |
41 | | eqid 2736 |
. . . . . . . 8
β’ βͺ (KQβπ½) = βͺ
(KQβπ½) |
42 | 41 | t1sep2 22720 |
. . . . . . 7
β’
(((KQβπ½)
β Fre β§ (πΉβπ§) β βͺ
(KQβπ½) β§ (πΉβπ€) β βͺ
(KQβπ½)) β
(βπ£ β
(KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€))) |
43 | 30, 37, 40, 42 | syl3anc 1371 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€))) |
44 | 29, 43 | syld 47 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (βπ β π½ (π§ β π β π€ β π) β (πΉβπ§) = (πΉβπ€))) |
45 | 1 | kqfeq 23075 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π€ β π) β ((πΉβπ§) = (πΉβπ€) β βπ¦ β π½ (π§ β π¦ β π€ β π¦))) |
46 | | eleq2 2826 |
. . . . . . . . . 10
β’ (π = π¦ β (π§ β π β π§ β π¦)) |
47 | | eleq2 2826 |
. . . . . . . . . 10
β’ (π = π¦ β (π€ β π β π€ β π¦)) |
48 | 46, 47 | bibi12d 345 |
. . . . . . . . 9
β’ (π = π¦ β ((π§ β π β π€ β π) β (π§ β π¦ β π€ β π¦))) |
49 | 48 | cbvralvw 3225 |
. . . . . . . 8
β’
(βπ β
π½ (π§ β π β π€ β π) β βπ¦ β π½ (π§ β π¦ β π€ β π¦)) |
50 | 45, 49 | bitr4di 288 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π€ β π) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
51 | 50 | 3expb 1120 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ (π§ β π β§ π€ β π)) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
52 | 51 | adantlr 713 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
53 | 44, 52 | sylibd 238 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β§ (π§ β π β§ π€ β π)) β (βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π))) |
54 | 53 | ralrimivva 3197 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (KQβπ½) β Fre) β
βπ§ β π βπ€ β π (βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π))) |
55 | 54 | ex 413 |
. 2
β’ (π½ β (TopOnβπ) β ((KQβπ½) β Fre β
βπ§ β π βπ€ β π (βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π)))) |
56 | 1 | kqopn 23085 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ π β π½) β (πΉ β π) β (KQβπ½)) |
57 | 56 | ad4ant14 750 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β§ π β π½) β (πΉ β π) β (KQβπ½)) |
58 | | eleq2 2826 |
. . . . . . . . . . . 12
β’ (π£ = (πΉ β π) β ((πΉβπ§) β π£ β (πΉβπ§) β (πΉ β π))) |
59 | | eleq2 2826 |
. . . . . . . . . . . 12
β’ (π£ = (πΉ β π) β ((πΉβπ€) β π£ β (πΉβπ€) β (πΉ β π))) |
60 | 58, 59 | imbi12d 344 |
. . . . . . . . . . 11
β’ (π£ = (πΉ β π) β (((πΉβπ§) β π£ β (πΉβπ€) β π£) β ((πΉβπ§) β (πΉ β π) β (πΉβπ€) β (πΉ β π)))) |
61 | 60 | rspcv 3577 |
. . . . . . . . . 10
β’ ((πΉ β π) β (KQβπ½) β (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β ((πΉβπ§) β (πΉ β π) β (πΉβπ€) β (πΉ β π)))) |
62 | 57, 61 | syl 17 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β§ π β π½) β (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β ((πΉβπ§) β (πΉ β π) β (πΉβπ€) β (πΉ β π)))) |
63 | 1 | kqfvima 23081 |
. . . . . . . . . . . . 13
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π§ β π) β (π§ β π β (πΉβπ§) β (πΉ β π))) |
64 | 63 | 3expa 1118 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ π β π½) β§ π§ β π) β (π§ β π β (πΉβπ§) β (πΉ β π))) |
65 | 64 | an32s 650 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ π§ β π) β§ π β π½) β (π§ β π β (πΉβπ§) β (πΉ β π))) |
66 | 65 | adantlr 713 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β§ π β π½) β (π§ β π β (πΉβπ§) β (πΉ β π))) |
67 | 1 | kqfvima 23081 |
. . . . . . . . . . . . 13
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π€ β π) β (π€ β π β (πΉβπ€) β (πΉ β π))) |
68 | 67 | 3expa 1118 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ π β π½) β§ π€ β π) β (π€ β π β (πΉβπ€) β (πΉ β π))) |
69 | 68 | an32s 650 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ π€ β π) β§ π β π½) β (π€ β π β (πΉβπ€) β (πΉ β π))) |
70 | 69 | adantllr 717 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β§ π β π½) β (π€ β π β (πΉβπ€) β (πΉ β π))) |
71 | 66, 70 | imbi12d 344 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β§ π β π½) β ((π§ β π β π€ β π) β ((πΉβπ§) β (πΉ β π) β (πΉβπ€) β (πΉ β π)))) |
72 | 62, 71 | sylibrd 258 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β§ π β π½) β (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (π§ β π β π€ β π))) |
73 | 72 | ralrimdva 3151 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β βπ β π½ (π§ β π β π€ β π))) |
74 | 1 | kqfval 23074 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ π§ β π) β (πΉβπ§) = {π¦ β π½ β£ π§ β π¦}) |
75 | 74 | adantr 481 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β (πΉβπ§) = {π¦ β π½ β£ π§ β π¦}) |
76 | 1 | kqfval 23074 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ π€ β π) β (πΉβπ€) = {π¦ β π½ β£ π€ β π¦}) |
77 | 76 | adantlr 713 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β (πΉβπ€) = {π¦ β π½ β£ π€ β π¦}) |
78 | 75, 77 | eqeq12d 2752 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β ((πΉβπ§) = (πΉβπ€) β {π¦ β π½ β£ π§ β π¦} = {π¦ β π½ β£ π€ β π¦})) |
79 | | rabbi 3432 |
. . . . . . . . . 10
β’
(βπ¦ β
π½ (π§ β π¦ β π€ β π¦) β {π¦ β π½ β£ π§ β π¦} = {π¦ β π½ β£ π€ β π¦}) |
80 | 49, 79 | bitri 274 |
. . . . . . . . 9
β’
(βπ β
π½ (π§ β π β π€ β π) β {π¦ β π½ β£ π§ β π¦} = {π¦ β π½ β£ π€ β π¦}) |
81 | 78, 80 | bitr4di 288 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β ((πΉβπ§) = (πΉβπ€) β βπ β π½ (π§ β π β π€ β π))) |
82 | 81 | biimprd 247 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β (βπ β π½ (π§ β π β π€ β π) β (πΉβπ§) = (πΉβπ€))) |
83 | 73, 82 | imim12d 81 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π§ β π) β§ π€ β π) β ((βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π)) β (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€)))) |
84 | 83 | ralimdva 3164 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π§ β π) β (βπ€ β π (βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π)) β βπ€ β π (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€)))) |
85 | 84 | ralimdva 3164 |
. . . 4
β’ (π½ β (TopOnβπ) β (βπ§ β π βπ€ β π (βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π)) β βπ§ β π βπ€ β π (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€)))) |
86 | | eleq1 2825 |
. . . . . . . . . . 11
β’ (π = (πΉβπ§) β (π β π£ β (πΉβπ§) β π£)) |
87 | 86 | imbi1d 341 |
. . . . . . . . . 10
β’ (π = (πΉβπ§) β ((π β π£ β π β π£) β ((πΉβπ§) β π£ β π β π£))) |
88 | 87 | ralbidv 3174 |
. . . . . . . . 9
β’ (π = (πΉβπ§) β (βπ£ β (KQβπ½)(π β π£ β π β π£) β βπ£ β (KQβπ½)((πΉβπ§) β π£ β π β π£))) |
89 | | eqeq1 2740 |
. . . . . . . . 9
β’ (π = (πΉβπ§) β (π = π β (πΉβπ§) = π)) |
90 | 88, 89 | imbi12d 344 |
. . . . . . . 8
β’ (π = (πΉβπ§) β ((βπ£ β (KQβπ½)(π β π£ β π β π£) β π = π) β (βπ£ β (KQβπ½)((πΉβπ§) β π£ β π β π£) β (πΉβπ§) = π))) |
91 | 90 | ralbidv 3174 |
. . . . . . 7
β’ (π = (πΉβπ§) β (βπ β ran πΉ(βπ£ β (KQβπ½)(π β π£ β π β π£) β π = π) β βπ β ran πΉ(βπ£ β (KQβπ½)((πΉβπ§) β π£ β π β π£) β (πΉβπ§) = π))) |
92 | 91 | ralrn 7038 |
. . . . . 6
β’ (πΉ Fn π β (βπ β ran πΉβπ β ran πΉ(βπ£ β (KQβπ½)(π β π£ β π β π£) β π = π) β βπ§ β π βπ β ran πΉ(βπ£ β (KQβπ½)((πΉβπ§) β π£ β π β π£) β (πΉβπ§) = π))) |
93 | | eleq1 2825 |
. . . . . . . . . . 11
β’ (π = (πΉβπ€) β (π β π£ β (πΉβπ€) β π£)) |
94 | 93 | imbi2d 340 |
. . . . . . . . . 10
β’ (π = (πΉβπ€) β (((πΉβπ§) β π£ β π β π£) β ((πΉβπ§) β π£ β (πΉβπ€) β π£))) |
95 | 94 | ralbidv 3174 |
. . . . . . . . 9
β’ (π = (πΉβπ€) β (βπ£ β (KQβπ½)((πΉβπ§) β π£ β π β π£) β βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£))) |
96 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π = (πΉβπ€) β ((πΉβπ§) = π β (πΉβπ§) = (πΉβπ€))) |
97 | 95, 96 | imbi12d 344 |
. . . . . . . 8
β’ (π = (πΉβπ€) β ((βπ£ β (KQβπ½)((πΉβπ§) β π£ β π β π£) β (πΉβπ§) = π) β (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€)))) |
98 | 97 | ralrn 7038 |
. . . . . . 7
β’ (πΉ Fn π β (βπ β ran πΉ(βπ£ β (KQβπ½)((πΉβπ§) β π£ β π β π£) β (πΉβπ§) = π) β βπ€ β π (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€)))) |
99 | 98 | ralbidv 3174 |
. . . . . 6
β’ (πΉ Fn π β (βπ§ β π βπ β ran πΉ(βπ£ β (KQβπ½)((πΉβπ§) β π£ β π β π£) β (πΉβπ§) = π) β βπ§ β π βπ€ β π (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€)))) |
100 | 92, 99 | bitrd 278 |
. . . . 5
β’ (πΉ Fn π β (βπ β ran πΉβπ β ran πΉ(βπ£ β (KQβπ½)(π β π£ β π β π£) β π = π) β βπ§ β π βπ€ β π (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€)))) |
101 | 11, 100 | syl 17 |
. . . 4
β’ (π½ β (TopOnβπ) β (βπ β ran πΉβπ β ran πΉ(βπ£ β (KQβπ½)(π β π£ β π β π£) β π = π) β βπ§ β π βπ€ β π (βπ£ β (KQβπ½)((πΉβπ§) β π£ β (πΉβπ€) β π£) β (πΉβπ§) = (πΉβπ€)))) |
102 | 85, 101 | sylibrd 258 |
. . 3
β’ (π½ β (TopOnβπ) β (βπ§ β π βπ€ β π (βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π)) β βπ β ran πΉβπ β ran πΉ(βπ£ β (KQβπ½)(π β π£ β π β π£) β π = π))) |
103 | | ist1-2 22698 |
. . . 4
β’
((KQβπ½) β
(TopOnβran πΉ) β
((KQβπ½) β Fre
β βπ β ran
πΉβπ β ran πΉ(βπ£ β (KQβπ½)(π β π£ β π β π£) β π = π))) |
104 | 33, 103 | syl 17 |
. . 3
β’ (π½ β (TopOnβπ) β ((KQβπ½) β Fre β
βπ β ran πΉβπ β ran πΉ(βπ£ β (KQβπ½)(π β π£ β π β π£) β π = π))) |
105 | 102, 104 | sylibrd 258 |
. 2
β’ (π½ β (TopOnβπ) β (βπ§ β π βπ€ β π (βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π)) β (KQβπ½) β Fre)) |
106 | 55, 105 | impbid 211 |
1
β’ (π½ β (TopOnβπ) β ((KQβπ½) β Fre β
βπ§ β π βπ€ β π (βπ β π½ (π§ β π β π€ β π) β βπ β π½ (π§ β π β π€ β π)))) |