Step | Hyp | Ref
| Expression |
1 | | kqval.2 |
. . . . . . . . . 10
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) |
2 | 1 | kqopn 23085 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ π€ β π½) β (πΉ β π€) β (KQβπ½)) |
3 | 2 | adantlr 713 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ (π β π β§ π β π)) β§ π€ β π½) β (πΉ β π€) β (KQβπ½)) |
4 | | eleq2 2826 |
. . . . . . . . . 10
β’ (π§ = (πΉ β π€) β ((πΉβπ) β π§ β (πΉβπ) β (πΉ β π€))) |
5 | | eleq2 2826 |
. . . . . . . . . 10
β’ (π§ = (πΉ β π€) β ((πΉβπ) β π§ β (πΉβπ) β (πΉ β π€))) |
6 | 4, 5 | bibi12d 345 |
. . . . . . . . 9
β’ (π§ = (πΉ β π€) β (((πΉβπ) β π§ β (πΉβπ) β π§) β ((πΉβπ) β (πΉ β π€) β (πΉβπ) β (πΉ β π€)))) |
7 | 6 | rspcv 3577 |
. . . . . . . 8
β’ ((πΉ β π€) β (KQβπ½) β (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β ((πΉβπ) β (πΉ β π€) β (πΉβπ) β (πΉ β π€)))) |
8 | 3, 7 | syl 17 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ (π β π β§ π β π)) β§ π€ β π½) β (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β ((πΉβπ) β (πΉ β π€) β (πΉβπ) β (πΉ β π€)))) |
9 | 1 | kqfvima 23081 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ π€ β π½ β§ π β π) β (π β π€ β (πΉβπ) β (πΉ β π€))) |
10 | 9 | 3expa 1118 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ π€ β π½) β§ π β π) β (π β π€ β (πΉβπ) β (πΉ β π€))) |
11 | 10 | adantrr 715 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π€ β π½) β§ (π β π β§ π β π)) β (π β π€ β (πΉβπ) β (πΉ β π€))) |
12 | 1 | kqfvima 23081 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ π€ β π½ β§ π β π) β (π β π€ β (πΉβπ) β (πΉ β π€))) |
13 | 12 | 3expa 1118 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ π€ β π½) β§ π β π) β (π β π€ β (πΉβπ) β (πΉ β π€))) |
14 | 13 | adantrl 714 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π€ β π½) β§ (π β π β§ π β π)) β (π β π€ β (πΉβπ) β (πΉ β π€))) |
15 | 11, 14 | bibi12d 345 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π€ β π½) β§ (π β π β§ π β π)) β ((π β π€ β π β π€) β ((πΉβπ) β (πΉ β π€) β (πΉβπ) β (πΉ β π€)))) |
16 | 15 | an32s 650 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ (π β π β§ π β π)) β§ π€ β π½) β ((π β π€ β π β π€) β ((πΉβπ) β (πΉ β π€) β (πΉβπ) β (πΉ β π€)))) |
17 | 8, 16 | sylibrd 258 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ (π β π β§ π β π)) β§ π€ β π½) β (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β (π β π€ β π β π€))) |
18 | 17 | ralrimdva 3151 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (π β π β§ π β π)) β (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β βπ€ β π½ (π β π€ β π β π€))) |
19 | 1 | kqfeq 23075 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π β π β§ π β π) β ((πΉβπ) = (πΉβπ) β βπ¦ β π½ (π β π¦ β π β π¦))) |
20 | 19 | 3expb 1120 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ (π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β βπ¦ β π½ (π β π¦ β π β π¦))) |
21 | | elequ2 2121 |
. . . . . . . 8
β’ (π¦ = π€ β (π β π¦ β π β π€)) |
22 | | elequ2 2121 |
. . . . . . . 8
β’ (π¦ = π€ β (π β π¦ β π β π€)) |
23 | 21, 22 | bibi12d 345 |
. . . . . . 7
β’ (π¦ = π€ β ((π β π¦ β π β π¦) β (π β π€ β π β π€))) |
24 | 23 | cbvralvw 3225 |
. . . . . 6
β’
(βπ¦ β
π½ (π β π¦ β π β π¦) β βπ€ β π½ (π β π€ β π β π€)) |
25 | 20, 24 | bitrdi 286 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β βπ€ β π½ (π β π€ β π β π€))) |
26 | 18, 25 | sylibrd 258 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ (π β π β§ π β π)) β (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β (πΉβπ) = (πΉβπ))) |
27 | 26 | ralrimivva 3197 |
. . 3
β’ (π½ β (TopOnβπ) β βπ β π βπ β π (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β (πΉβπ) = (πΉβπ))) |
28 | 1 | kqffn 23076 |
. . . 4
β’ (π½ β (TopOnβπ) β πΉ Fn π) |
29 | | eleq1 2825 |
. . . . . . . . . 10
β’ (π’ = (πΉβπ) β (π’ β π§ β (πΉβπ) β π§)) |
30 | 29 | bibi1d 343 |
. . . . . . . . 9
β’ (π’ = (πΉβπ) β ((π’ β π§ β π£ β π§) β ((πΉβπ) β π§ β π£ β π§))) |
31 | 30 | ralbidv 3174 |
. . . . . . . 8
β’ (π’ = (πΉβπ) β (βπ§ β (KQβπ½)(π’ β π§ β π£ β π§) β βπ§ β (KQβπ½)((πΉβπ) β π§ β π£ β π§))) |
32 | | eqeq1 2740 |
. . . . . . . 8
β’ (π’ = (πΉβπ) β (π’ = π£ β (πΉβπ) = π£)) |
33 | 31, 32 | imbi12d 344 |
. . . . . . 7
β’ (π’ = (πΉβπ) β ((βπ§ β (KQβπ½)(π’ β π§ β π£ β π§) β π’ = π£) β (βπ§ β (KQβπ½)((πΉβπ) β π§ β π£ β π§) β (πΉβπ) = π£))) |
34 | 33 | ralbidv 3174 |
. . . . . 6
β’ (π’ = (πΉβπ) β (βπ£ β ran πΉ(βπ§ β (KQβπ½)(π’ β π§ β π£ β π§) β π’ = π£) β βπ£ β ran πΉ(βπ§ β (KQβπ½)((πΉβπ) β π§ β π£ β π§) β (πΉβπ) = π£))) |
35 | 34 | ralrn 7038 |
. . . . 5
β’ (πΉ Fn π β (βπ’ β ran πΉβπ£ β ran πΉ(βπ§ β (KQβπ½)(π’ β π§ β π£ β π§) β π’ = π£) β βπ β π βπ£ β ran πΉ(βπ§ β (KQβπ½)((πΉβπ) β π§ β π£ β π§) β (πΉβπ) = π£))) |
36 | | eleq1 2825 |
. . . . . . . . . 10
β’ (π£ = (πΉβπ) β (π£ β π§ β (πΉβπ) β π§)) |
37 | 36 | bibi2d 342 |
. . . . . . . . 9
β’ (π£ = (πΉβπ) β (((πΉβπ) β π§ β π£ β π§) β ((πΉβπ) β π§ β (πΉβπ) β π§))) |
38 | 37 | ralbidv 3174 |
. . . . . . . 8
β’ (π£ = (πΉβπ) β (βπ§ β (KQβπ½)((πΉβπ) β π§ β π£ β π§) β βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§))) |
39 | | eqeq2 2748 |
. . . . . . . 8
β’ (π£ = (πΉβπ) β ((πΉβπ) = π£ β (πΉβπ) = (πΉβπ))) |
40 | 38, 39 | imbi12d 344 |
. . . . . . 7
β’ (π£ = (πΉβπ) β ((βπ§ β (KQβπ½)((πΉβπ) β π§ β π£ β π§) β (πΉβπ) = π£) β (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β (πΉβπ) = (πΉβπ)))) |
41 | 40 | ralrn 7038 |
. . . . . 6
β’ (πΉ Fn π β (βπ£ β ran πΉ(βπ§ β (KQβπ½)((πΉβπ) β π§ β π£ β π§) β (πΉβπ) = π£) β βπ β π (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β (πΉβπ) = (πΉβπ)))) |
42 | 41 | ralbidv 3174 |
. . . . 5
β’ (πΉ Fn π β (βπ β π βπ£ β ran πΉ(βπ§ β (KQβπ½)((πΉβπ) β π§ β π£ β π§) β (πΉβπ) = π£) β βπ β π βπ β π (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β (πΉβπ) = (πΉβπ)))) |
43 | 35, 42 | bitrd 278 |
. . . 4
β’ (πΉ Fn π β (βπ’ β ran πΉβπ£ β ran πΉ(βπ§ β (KQβπ½)(π’ β π§ β π£ β π§) β π’ = π£) β βπ β π βπ β π (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β (πΉβπ) = (πΉβπ)))) |
44 | 28, 43 | syl 17 |
. . 3
β’ (π½ β (TopOnβπ) β (βπ’ β ran πΉβπ£ β ran πΉ(βπ§ β (KQβπ½)(π’ β π§ β π£ β π§) β π’ = π£) β βπ β π βπ β π (βπ§ β (KQβπ½)((πΉβπ) β π§ β (πΉβπ) β π§) β (πΉβπ) = (πΉβπ)))) |
45 | 27, 44 | mpbird 256 |
. 2
β’ (π½ β (TopOnβπ) β βπ’ β ran πΉβπ£ β ran πΉ(βπ§ β (KQβπ½)(π’ β π§ β π£ β π§) β π’ = π£)) |
46 | 1 | kqtopon 23078 |
. . 3
β’ (π½ β (TopOnβπ) β (KQβπ½) β (TopOnβran πΉ)) |
47 | | ist0-2 22695 |
. . 3
β’
((KQβπ½) β
(TopOnβran πΉ) β
((KQβπ½) β Kol2
β βπ’ β ran
πΉβπ£ β ran πΉ(βπ§ β (KQβπ½)(π’ β π§ β π£ β π§) β π’ = π£))) |
48 | 46, 47 | syl 17 |
. 2
β’ (π½ β (TopOnβπ) β ((KQβπ½) β Kol2 β
βπ’ β ran πΉβπ£ β ran πΉ(βπ§ β (KQβπ½)(π’ β π§ β π£ β π§) β π’ = π£))) |
49 | 45, 48 | mpbird 256 |
1
β’ (π½ β (TopOnβπ) β (KQβπ½) β Kol2) |