Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . 6
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
2 | 1 | kqfeq 23729 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π€ β π) β ((πΉβπ§) = (πΉβπ€) β βπ¦ β π½ (π§ β π¦ β π€ β π¦))) |
3 | 2 | 3expb 1117 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ (π§ β π β§ π€ β π)) β ((πΉβπ§) = (πΉβπ€) β βπ¦ β π½ (π§ β π¦ β π€ β π¦))) |
4 | 3 | imbi1d 340 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (π§ β π β§ π€ β π)) β (((πΉβπ§) = (πΉβπ€) β π§ = π€) β (βπ¦ β π½ (π§ β π¦ β π€ β π¦) β π§ = π€))) |
5 | 4 | 2ralbidva 3210 |
. 2
β’ (π½ β (TopOnβπ) β (βπ§ β π βπ€ β π ((πΉβπ§) = (πΉβπ€) β π§ = π€) β βπ§ β π βπ€ β π (βπ¦ β π½ (π§ β π¦ β π€ β π¦) β π§ = π€))) |
6 | 1 | kqffn 23730 |
. . . 4
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
7 | | dffn2 6731 |
. . . 4
β’ (πΉ Fn π β πΉ:πβΆV) |
8 | 6, 7 | sylib 217 |
. . 3
β’ (π½ β (TopOnβπ) β πΉ:πβΆV) |
9 | | dff13 7271 |
. . . 4
β’ (πΉ:πβ1-1βV β (πΉ:πβΆV β§ βπ§ β π βπ€ β π ((πΉβπ§) = (πΉβπ€) β π§ = π€))) |
10 | 9 | baib 534 |
. . 3
β’ (πΉ:πβΆV β (πΉ:πβ1-1βV β βπ§ β π βπ€ β π ((πΉβπ§) = (πΉβπ€) β π§ = π€))) |
11 | 8, 10 | syl 17 |
. 2
β’ (π½ β (TopOnβπ) β (πΉ:πβ1-1βV β βπ§ β π βπ€ β π ((πΉβπ§) = (πΉβπ€) β π§ = π€))) |
12 | | ist0-2 23349 |
. 2
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β βπ§ β π βπ€ β π (βπ¦ β π½ (π§ β π¦ β π€ β π¦) β π§ = π€))) |
13 | 5, 11, 12 | 3bitr4rd 311 |
1
β’ (π½ β (TopOnβπ) β (π½ β Kol2 β πΉ:πβ1-1βV)) |