Step |
Hyp |
Ref |
Expression |
1 |
|
eltpsi.k |
|- K = { <. ( Base ` ndx ) , A >. , <. ( TopSet ` ndx ) , J >. } |
2 |
|
basendxlttsetndx |
|- ( Base ` ndx ) < ( TopSet ` ndx ) |
3 |
|
tsetndxnn |
|- ( TopSet ` ndx ) e. NN |
4 |
|
tsetid |
|- TopSet = Slot ( TopSet ` ndx ) |
5 |
1 2 3 4
|
2strop1 |
|- ( J e. ( TopOn ` A ) -> J = ( TopSet ` K ) ) |
6 |
|
toponmax |
|- ( J e. ( TopOn ` A ) -> A e. J ) |
7 |
1 2 3
|
2strbas1 |
|- ( A e. J -> A = ( Base ` K ) ) |
8 |
6 7
|
syl |
|- ( J e. ( TopOn ` A ) -> A = ( Base ` K ) ) |
9 |
8
|
fveq2d |
|- ( J e. ( TopOn ` A ) -> ( TopOn ` A ) = ( TopOn ` ( Base ` K ) ) ) |
10 |
5 9
|
eleq12d |
|- ( J e. ( TopOn ` A ) -> ( J e. ( TopOn ` A ) <-> ( TopSet ` K ) e. ( TopOn ` ( Base ` K ) ) ) ) |
11 |
10
|
ibi |
|- ( J e. ( TopOn ` A ) -> ( TopSet ` K ) e. ( TopOn ` ( Base ` K ) ) ) |
12 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
13 |
|
eqid |
|- ( TopSet ` K ) = ( TopSet ` K ) |
14 |
12 13
|
tsettps |
|- ( ( TopSet ` K ) e. ( TopOn ` ( Base ` K ) ) -> K e. TopSp ) |
15 |
11 14
|
syl |
|- ( J e. ( TopOn ` A ) -> K e. TopSp ) |