Step |
Hyp |
Ref |
Expression |
1 |
|
ptuniconst.2 |
|- J = ( Xt_ ` ( A X. { R } ) ) |
2 |
|
id |
|- ( R e. ( TopOn ` X ) -> R e. ( TopOn ` X ) ) |
3 |
2
|
ralrimivw |
|- ( R e. ( TopOn ` X ) -> A. x e. A R e. ( TopOn ` X ) ) |
4 |
|
fconstmpt |
|- ( A X. { R } ) = ( x e. A |-> R ) |
5 |
4
|
fveq2i |
|- ( Xt_ ` ( A X. { R } ) ) = ( Xt_ ` ( x e. A |-> R ) ) |
6 |
1 5
|
eqtri |
|- J = ( Xt_ ` ( x e. A |-> R ) ) |
7 |
6
|
pttopon |
|- ( ( A e. V /\ A. x e. A R e. ( TopOn ` X ) ) -> J e. ( TopOn ` X_ x e. A X ) ) |
8 |
3 7
|
sylan2 |
|- ( ( A e. V /\ R e. ( TopOn ` X ) ) -> J e. ( TopOn ` X_ x e. A X ) ) |
9 |
|
toponmax |
|- ( R e. ( TopOn ` X ) -> X e. R ) |
10 |
|
ixpconstg |
|- ( ( A e. V /\ X e. R ) -> X_ x e. A X = ( X ^m A ) ) |
11 |
9 10
|
sylan2 |
|- ( ( A e. V /\ R e. ( TopOn ` X ) ) -> X_ x e. A X = ( X ^m A ) ) |
12 |
11
|
fveq2d |
|- ( ( A e. V /\ R e. ( TopOn ` X ) ) -> ( TopOn ` X_ x e. A X ) = ( TopOn ` ( X ^m A ) ) ) |
13 |
8 12
|
eleqtrd |
|- ( ( A e. V /\ R e. ( TopOn ` X ) ) -> J e. ( TopOn ` ( X ^m A ) ) ) |