Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . 5
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
2 | 1 | kqffn 23079 |
. . . 4
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
3 | 2 | 3ad2ant1 1134 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β πΉ Fn π) |
4 | | toponss 22279 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π β π½) β π β π) |
5 | 4 | 3adant3 1133 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β π β π) |
6 | | fnfvima 7184 |
. . . 4
β’ ((πΉ Fn π β§ π β π β§ π΄ β π) β (πΉβπ΄) β (πΉ β π)) |
7 | 6 | 3expia 1122 |
. . 3
β’ ((πΉ Fn π β§ π β π) β (π΄ β π β (πΉβπ΄) β (πΉ β π))) |
8 | 3, 5, 7 | syl2anc 585 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β (π΄ β π β (πΉβπ΄) β (πΉ β π))) |
9 | | fnfun 6603 |
. . . 4
β’ (πΉ Fn π β Fun πΉ) |
10 | | fvelima 6909 |
. . . . 5
β’ ((Fun
πΉ β§ (πΉβπ΄) β (πΉ β π)) β βπ§ β π (πΉβπ§) = (πΉβπ΄)) |
11 | 10 | ex 414 |
. . . 4
β’ (Fun
πΉ β ((πΉβπ΄) β (πΉ β π) β βπ§ β π (πΉβπ§) = (πΉβπ΄))) |
12 | 3, 9, 11 | 3syl 18 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β ((πΉβπ΄) β (πΉ β π) β βπ§ β π (πΉβπ§) = (πΉβπ΄))) |
13 | | simpl1 1192 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β π½ β (TopOnβπ)) |
14 | 5 | sselda 3945 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β π§ β π) |
15 | | simpl3 1194 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β π΄ β π) |
16 | 1 | kqfeq 23078 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ π§ β π β§ π΄ β π) β ((πΉβπ§) = (πΉβπ΄) β βπ¦ β π½ (π§ β π¦ β π΄ β π¦))) |
17 | 13, 14, 15, 16 | syl3anc 1372 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β ((πΉβπ§) = (πΉβπ΄) β βπ¦ β π½ (π§ β π¦ β π΄ β π¦))) |
18 | | eleq2 2827 |
. . . . . . . . 9
β’ (π¦ = π€ β (π§ β π¦ β π§ β π€)) |
19 | | eleq2 2827 |
. . . . . . . . 9
β’ (π¦ = π€ β (π΄ β π¦ β π΄ β π€)) |
20 | 18, 19 | bibi12d 346 |
. . . . . . . 8
β’ (π¦ = π€ β ((π§ β π¦ β π΄ β π¦) β (π§ β π€ β π΄ β π€))) |
21 | 20 | cbvralvw 3226 |
. . . . . . 7
β’
(βπ¦ β
π½ (π§ β π¦ β π΄ β π¦) β βπ€ β π½ (π§ β π€ β π΄ β π€)) |
22 | 17, 21 | bitrdi 287 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β ((πΉβπ§) = (πΉβπ΄) β βπ€ β π½ (π§ β π€ β π΄ β π€))) |
23 | | simpl2 1193 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β π β π½) |
24 | | eleq2 2827 |
. . . . . . . . 9
β’ (π€ = π β (π§ β π€ β π§ β π)) |
25 | | eleq2 2827 |
. . . . . . . . 9
β’ (π€ = π β (π΄ β π€ β π΄ β π)) |
26 | 24, 25 | bibi12d 346 |
. . . . . . . 8
β’ (π€ = π β ((π§ β π€ β π΄ β π€) β (π§ β π β π΄ β π))) |
27 | 26 | rspcv 3578 |
. . . . . . 7
β’ (π β π½ β (βπ€ β π½ (π§ β π€ β π΄ β π€) β (π§ β π β π΄ β π))) |
28 | 23, 27 | syl 17 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β (βπ€ β π½ (π§ β π€ β π΄ β π€) β (π§ β π β π΄ β π))) |
29 | 22, 28 | sylbid 239 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β ((πΉβπ§) = (πΉβπ΄) β (π§ β π β π΄ β π))) |
30 | | simpr 486 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β π§ β π) |
31 | | biimp 214 |
. . . . 5
β’ ((π§ β π β π΄ β π) β (π§ β π β π΄ β π)) |
32 | 29, 30, 31 | syl6ci 71 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β§ π§ β π) β ((πΉβπ§) = (πΉβπ΄) β π΄ β π)) |
33 | 32 | rexlimdva 3153 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β (βπ§ β π (πΉβπ§) = (πΉβπ΄) β π΄ β π)) |
34 | 12, 33 | syld 47 |
. 2
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β ((πΉβπ΄) β (πΉ β π) β π΄ β π)) |
35 | 8, 34 | impbid 211 |
1
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β (π΄ β π β (πΉβπ΄) β (πΉ β π))) |