Step |
Hyp |
Ref |
Expression |
1 |
|
t0kq.1 |
|- F = ( x e. X |-> { y e. J | x e. y } ) |
2 |
|
simpl |
|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> J e. ( TopOn ` X ) ) |
3 |
1
|
ist0-4 |
|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> F : X -1-1-> _V ) ) |
4 |
3
|
biimpa |
|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> F : X -1-1-> _V ) |
5 |
2 4
|
qtopf1 |
|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> F e. ( J Homeo ( J qTop F ) ) ) |
6 |
1
|
kqval |
|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) = ( J qTop F ) ) |
7 |
6
|
adantr |
|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> ( KQ ` J ) = ( J qTop F ) ) |
8 |
7
|
oveq2d |
|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> ( J Homeo ( KQ ` J ) ) = ( J Homeo ( J qTop F ) ) ) |
9 |
5 8
|
eleqtrrd |
|- ( ( J e. ( TopOn ` X ) /\ J e. Kol2 ) -> F e. ( J Homeo ( KQ ` J ) ) ) |
10 |
|
hmphi |
|- ( F e. ( J Homeo ( KQ ` J ) ) -> J ~= ( KQ ` J ) ) |
11 |
|
hmphsym |
|- ( J ~= ( KQ ` J ) -> ( KQ ` J ) ~= J ) |
12 |
10 11
|
syl |
|- ( F e. ( J Homeo ( KQ ` J ) ) -> ( KQ ` J ) ~= J ) |
13 |
1
|
kqt0lem |
|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. Kol2 ) |
14 |
|
t0hmph |
|- ( ( KQ ` J ) ~= J -> ( ( KQ ` J ) e. Kol2 -> J e. Kol2 ) ) |
15 |
12 13 14
|
syl2im |
|- ( F e. ( J Homeo ( KQ ` J ) ) -> ( J e. ( TopOn ` X ) -> J e. Kol2 ) ) |
16 |
15
|
impcom |
|- ( ( J e. ( TopOn ` X ) /\ F e. ( J Homeo ( KQ ` J ) ) ) -> J e. Kol2 ) |
17 |
9 16
|
impbida |
|- ( J e. ( TopOn ` X ) -> ( J e. Kol2 <-> F e. ( J Homeo ( KQ ` J ) ) ) ) |