# Metamath Proof Explorer

## Theorem xpstopnlem1

Description: The function F used in xpsval is a homeomorphism from the binary product topology to the indexed product topology. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses xpstopnlem1.f
`|- F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )`
xpstopnlem1.j
`|- ( ph -> J e. ( TopOn ` X ) )`
xpstopnlem1.k
`|- ( ph -> K e. ( TopOn ` Y ) )`
Assertion xpstopnlem1
`|- ( ph -> F e. ( ( J tX K ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) )`

### Proof

Step Hyp Ref Expression
1 xpstopnlem1.f
` |-  F = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } )`
2 xpstopnlem1.j
` |-  ( ph -> J e. ( TopOn ` X ) )`
3 xpstopnlem1.k
` |-  ( ph -> K e. ( TopOn ` Y ) )`
4 txtopon
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )`
5 2 3 4 syl2anc
` |-  ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )`
6 eqid
` |-  ( Xt_ ` { <. (/) , J >. } ) = ( Xt_ ` { <. (/) , J >. } )`
7 0ex
` |-  (/) e. _V`
8 7 a1i
` |-  ( ph -> (/) e. _V )`
9 6 8 2 pt1hmeo
` |-  ( ph -> ( z e. X |-> { <. (/) , z >. } ) e. ( J Homeo ( Xt_ ` { <. (/) , J >. } ) ) )`
10 hmeocn
` |-  ( ( z e. X |-> { <. (/) , z >. } ) e. ( J Homeo ( Xt_ ` { <. (/) , J >. } ) ) -> ( z e. X |-> { <. (/) , z >. } ) e. ( J Cn ( Xt_ ` { <. (/) , J >. } ) ) )`
11 cntop2
` |-  ( ( z e. X |-> { <. (/) , z >. } ) e. ( J Cn ( Xt_ ` { <. (/) , J >. } ) ) -> ( Xt_ ` { <. (/) , J >. } ) e. Top )`
12 9 10 11 3syl
` |-  ( ph -> ( Xt_ ` { <. (/) , J >. } ) e. Top )`
13 toptopon2
` |-  ( ( Xt_ ` { <. (/) , J >. } ) e. Top <-> ( Xt_ ` { <. (/) , J >. } ) e. ( TopOn ` U. ( Xt_ ` { <. (/) , J >. } ) ) )`
14 12 13 sylib
` |-  ( ph -> ( Xt_ ` { <. (/) , J >. } ) e. ( TopOn ` U. ( Xt_ ` { <. (/) , J >. } ) ) )`
15 eqid
` |-  ( Xt_ ` { <. 1o , K >. } ) = ( Xt_ ` { <. 1o , K >. } )`
16 1on
` |-  1o e. On`
17 16 a1i
` |-  ( ph -> 1o e. On )`
18 15 17 3 pt1hmeo
` |-  ( ph -> ( z e. Y |-> { <. 1o , z >. } ) e. ( K Homeo ( Xt_ ` { <. 1o , K >. } ) ) )`
19 hmeocn
` |-  ( ( z e. Y |-> { <. 1o , z >. } ) e. ( K Homeo ( Xt_ ` { <. 1o , K >. } ) ) -> ( z e. Y |-> { <. 1o , z >. } ) e. ( K Cn ( Xt_ ` { <. 1o , K >. } ) ) )`
20 cntop2
` |-  ( ( z e. Y |-> { <. 1o , z >. } ) e. ( K Cn ( Xt_ ` { <. 1o , K >. } ) ) -> ( Xt_ ` { <. 1o , K >. } ) e. Top )`
21 18 19 20 3syl
` |-  ( ph -> ( Xt_ ` { <. 1o , K >. } ) e. Top )`
22 toptopon2
` |-  ( ( Xt_ ` { <. 1o , K >. } ) e. Top <-> ( Xt_ ` { <. 1o , K >. } ) e. ( TopOn ` U. ( Xt_ ` { <. 1o , K >. } ) ) )`
23 21 22 sylib
` |-  ( ph -> ( Xt_ ` { <. 1o , K >. } ) e. ( TopOn ` U. ( Xt_ ` { <. 1o , K >. } ) ) )`
24 txtopon
` |-  ( ( ( Xt_ ` { <. (/) , J >. } ) e. ( TopOn ` U. ( Xt_ ` { <. (/) , J >. } ) ) /\ ( Xt_ ` { <. 1o , K >. } ) e. ( TopOn ` U. ( Xt_ ` { <. 1o , K >. } ) ) ) -> ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) e. ( TopOn ` ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) ) )`
25 14 23 24 syl2anc
` |-  ( ph -> ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) e. ( TopOn ` ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) ) )`
26 opeq2
` |-  ( z = x -> <. (/) , z >. = <. (/) , x >. )`
27 26 sneqd
` |-  ( z = x -> { <. (/) , z >. } = { <. (/) , x >. } )`
28 eqid
` |-  ( z e. X |-> { <. (/) , z >. } ) = ( z e. X |-> { <. (/) , z >. } )`
29 snex
` |-  { <. (/) , x >. } e. _V`
30 27 28 29 fvmpt
` |-  ( x e. X -> ( ( z e. X |-> { <. (/) , z >. } ) ` x ) = { <. (/) , x >. } )`
31 opeq2
` |-  ( z = y -> <. 1o , z >. = <. 1o , y >. )`
32 31 sneqd
` |-  ( z = y -> { <. 1o , z >. } = { <. 1o , y >. } )`
33 eqid
` |-  ( z e. Y |-> { <. 1o , z >. } ) = ( z e. Y |-> { <. 1o , z >. } )`
34 snex
` |-  { <. 1o , y >. } e. _V`
35 32 33 34 fvmpt
` |-  ( y e. Y -> ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) = { <. 1o , y >. } )`
36 opeq12
` |-  ( ( ( ( z e. X |-> { <. (/) , z >. } ) ` x ) = { <. (/) , x >. } /\ ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) = { <. 1o , y >. } ) -> <. ( ( z e. X |-> { <. (/) , z >. } ) ` x ) , ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) >. = <. { <. (/) , x >. } , { <. 1o , y >. } >. )`
37 30 35 36 syl2an
` |-  ( ( x e. X /\ y e. Y ) -> <. ( ( z e. X |-> { <. (/) , z >. } ) ` x ) , ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) >. = <. { <. (/) , x >. } , { <. 1o , y >. } >. )`
38 37 mpoeq3ia
` |-  ( x e. X , y e. Y |-> <. ( ( z e. X |-> { <. (/) , z >. } ) ` x ) , ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) >. ) = ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. )`
39 toponuni
` |-  ( J e. ( TopOn ` X ) -> X = U. J )`
40 2 39 syl
` |-  ( ph -> X = U. J )`
41 toponuni
` |-  ( K e. ( TopOn ` Y ) -> Y = U. K )`
42 3 41 syl
` |-  ( ph -> Y = U. K )`
43 mpoeq12
` |-  ( ( X = U. J /\ Y = U. K ) -> ( x e. X , y e. Y |-> <. ( ( z e. X |-> { <. (/) , z >. } ) ` x ) , ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) >. ) = ( x e. U. J , y e. U. K |-> <. ( ( z e. X |-> { <. (/) , z >. } ) ` x ) , ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) >. ) )`
44 40 42 43 syl2anc
` |-  ( ph -> ( x e. X , y e. Y |-> <. ( ( z e. X |-> { <. (/) , z >. } ) ` x ) , ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) >. ) = ( x e. U. J , y e. U. K |-> <. ( ( z e. X |-> { <. (/) , z >. } ) ` x ) , ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) >. ) )`
45 38 44 syl5eqr
` |-  ( ph -> ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) = ( x e. U. J , y e. U. K |-> <. ( ( z e. X |-> { <. (/) , z >. } ) ` x ) , ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) >. ) )`
46 eqid
` |-  U. J = U. J`
47 eqid
` |-  U. K = U. K`
48 46 47 9 18 txhmeo
` |-  ( ph -> ( x e. U. J , y e. U. K |-> <. ( ( z e. X |-> { <. (/) , z >. } ) ` x ) , ( ( z e. Y |-> { <. 1o , z >. } ) ` y ) >. ) e. ( ( J tX K ) Homeo ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) ) )`
49 45 48 eqeltrd
` |-  ( ph -> ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) e. ( ( J tX K ) Homeo ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) ) )`
50 hmeocn
` |-  ( ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) e. ( ( J tX K ) Homeo ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) ) -> ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) e. ( ( J tX K ) Cn ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) ) )`
51 49 50 syl
` |-  ( ph -> ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) e. ( ( J tX K ) Cn ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) ) )`
52 cnf2
` |-  ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) e. ( TopOn ` ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) ) /\ ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) e. ( ( J tX K ) Cn ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) ) ) -> ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) : ( X X. Y ) --> ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) )`
53 5 25 51 52 syl3anc
` |-  ( ph -> ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) : ( X X. Y ) --> ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) )`
54 eqid
` |-  ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) = ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. )`
55 54 fmpo
` |-  ( A. x e. X A. y e. Y <. { <. (/) , x >. } , { <. 1o , y >. } >. e. ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) <-> ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) : ( X X. Y ) --> ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) )`
56 53 55 sylibr
` |-  ( ph -> A. x e. X A. y e. Y <. { <. (/) , x >. } , { <. 1o , y >. } >. e. ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) )`
57 56 r19.21bi
` |-  ( ( ph /\ x e. X ) -> A. y e. Y <. { <. (/) , x >. } , { <. 1o , y >. } >. e. ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) )`
58 57 r19.21bi
` |-  ( ( ( ph /\ x e. X ) /\ y e. Y ) -> <. { <. (/) , x >. } , { <. 1o , y >. } >. e. ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) )`
59 58 anasss
` |-  ( ( ph /\ ( x e. X /\ y e. Y ) ) -> <. { <. (/) , x >. } , { <. 1o , y >. } >. e. ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) )`
60 eqidd
` |-  ( ph -> ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) = ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) )`
61 vex
` |-  x e. _V`
62 vex
` |-  y e. _V`
63 61 62 op1std
` |-  ( z = <. x , y >. -> ( 1st ` z ) = x )`
64 61 62 op2ndd
` |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )`
65 63 64 uneq12d
` |-  ( z = <. x , y >. -> ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( x u. y ) )`
66 65 mpompt
` |-  ( z e. ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) |-> ( ( 1st ` z ) u. ( 2nd ` z ) ) ) = ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) )`
67 66 eqcomi
` |-  ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) ) = ( z e. ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) |-> ( ( 1st ` z ) u. ( 2nd ` z ) ) )`
68 67 a1i
` |-  ( ph -> ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) ) = ( z e. ( U. ( Xt_ ` { <. (/) , J >. } ) X. U. ( Xt_ ` { <. 1o , K >. } ) ) |-> ( ( 1st ` z ) u. ( 2nd ` z ) ) ) )`
69 29 34 op1std
` |-  ( z = <. { <. (/) , x >. } , { <. 1o , y >. } >. -> ( 1st ` z ) = { <. (/) , x >. } )`
70 29 34 op2ndd
` |-  ( z = <. { <. (/) , x >. } , { <. 1o , y >. } >. -> ( 2nd ` z ) = { <. 1o , y >. } )`
71 69 70 uneq12d
` |-  ( z = <. { <. (/) , x >. } , { <. 1o , y >. } >. -> ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( { <. (/) , x >. } u. { <. 1o , y >. } ) )`
72 df-pr
` |-  { <. (/) , x >. , <. 1o , y >. } = ( { <. (/) , x >. } u. { <. 1o , y >. } )`
73 71 72 eqtr4di
` |-  ( z = <. { <. (/) , x >. } , { <. 1o , y >. } >. -> ( ( 1st ` z ) u. ( 2nd ` z ) ) = { <. (/) , x >. , <. 1o , y >. } )`
74 59 60 68 73 fmpoco
` |-  ( ph -> ( ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) ) o. ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) ) = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) )`
75 1 74 eqtr4id
` |-  ( ph -> F = ( ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) ) o. ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) ) )`
76 eqid
` |-  U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) = U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) )`
77 eqid
` |-  U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) = U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) )`
78 eqid
` |-  ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) = ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } )`
79 eqid
` |-  ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) = ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) )`
80 eqid
` |-  ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) = ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) )`
81 eqid
` |-  ( x e. U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) , y e. U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) |-> ( x u. y ) ) = ( x e. U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) , y e. U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) |-> ( x u. y ) )`
82 2on
` |-  2o e. On`
83 82 a1i
` |-  ( ph -> 2o e. On )`
84 topontop
` |-  ( J e. ( TopOn ` X ) -> J e. Top )`
85 2 84 syl
` |-  ( ph -> J e. Top )`
86 topontop
` |-  ( K e. ( TopOn ` Y ) -> K e. Top )`
87 3 86 syl
` |-  ( ph -> K e. Top )`
88 xpscf
` |-  ( { <. (/) , J >. , <. 1o , K >. } : 2o --> Top <-> ( J e. Top /\ K e. Top ) )`
89 85 87 88 sylanbrc
` |-  ( ph -> { <. (/) , J >. , <. 1o , K >. } : 2o --> Top )`
90 df2o3
` |-  2o = { (/) , 1o }`
91 df-pr
` |-  { (/) , 1o } = ( { (/) } u. { 1o } )`
92 90 91 eqtri
` |-  2o = ( { (/) } u. { 1o } )`
93 92 a1i
` |-  ( ph -> 2o = ( { (/) } u. { 1o } ) )`
94 1n0
` |-  1o =/= (/)`
95 94 necomi
` |-  (/) =/= 1o`
96 disjsn2
` |-  ( (/) =/= 1o -> ( { (/) } i^i { 1o } ) = (/) )`
97 95 96 mp1i
` |-  ( ph -> ( { (/) } i^i { 1o } ) = (/) )`
98 76 77 78 79 80 81 83 89 93 97 ptunhmeo
` |-  ( ph -> ( x e. U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) , y e. U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) |-> ( x u. y ) ) e. ( ( ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) tX ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) )`
99 fnpr2o
` |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> { <. (/) , J >. , <. 1o , K >. } Fn 2o )`
100 2 3 99 syl2anc
` |-  ( ph -> { <. (/) , J >. , <. 1o , K >. } Fn 2o )`
101 7 prid1
` |-  (/) e. { (/) , 1o }`
102 101 90 eleqtrri
` |-  (/) e. 2o`
103 fnressn
` |-  ( ( { <. (/) , J >. , <. 1o , K >. } Fn 2o /\ (/) e. 2o ) -> ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) = { <. (/) , ( { <. (/) , J >. , <. 1o , K >. } ` (/) ) >. } )`
104 100 102 103 sylancl
` |-  ( ph -> ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) = { <. (/) , ( { <. (/) , J >. , <. 1o , K >. } ` (/) ) >. } )`
105 fvpr0o
` |-  ( J e. ( TopOn ` X ) -> ( { <. (/) , J >. , <. 1o , K >. } ` (/) ) = J )`
106 2 105 syl
` |-  ( ph -> ( { <. (/) , J >. , <. 1o , K >. } ` (/) ) = J )`
107 106 opeq2d
` |-  ( ph -> <. (/) , ( { <. (/) , J >. , <. 1o , K >. } ` (/) ) >. = <. (/) , J >. )`
108 107 sneqd
` |-  ( ph -> { <. (/) , ( { <. (/) , J >. , <. 1o , K >. } ` (/) ) >. } = { <. (/) , J >. } )`
109 104 108 eqtrd
` |-  ( ph -> ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) = { <. (/) , J >. } )`
110 109 fveq2d
` |-  ( ph -> ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) = ( Xt_ ` { <. (/) , J >. } ) )`
111 110 unieqd
` |-  ( ph -> U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) = U. ( Xt_ ` { <. (/) , J >. } ) )`
112 1oex
` |-  1o e. _V`
113 112 prid2
` |-  1o e. { (/) , 1o }`
114 113 90 eleqtrri
` |-  1o e. 2o`
115 fnressn
` |-  ( ( { <. (/) , J >. , <. 1o , K >. } Fn 2o /\ 1o e. 2o ) -> ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) = { <. 1o , ( { <. (/) , J >. , <. 1o , K >. } ` 1o ) >. } )`
116 100 114 115 sylancl
` |-  ( ph -> ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) = { <. 1o , ( { <. (/) , J >. , <. 1o , K >. } ` 1o ) >. } )`
117 fvpr1o
` |-  ( K e. ( TopOn ` Y ) -> ( { <. (/) , J >. , <. 1o , K >. } ` 1o ) = K )`
118 3 117 syl
` |-  ( ph -> ( { <. (/) , J >. , <. 1o , K >. } ` 1o ) = K )`
119 118 opeq2d
` |-  ( ph -> <. 1o , ( { <. (/) , J >. , <. 1o , K >. } ` 1o ) >. = <. 1o , K >. )`
120 119 sneqd
` |-  ( ph -> { <. 1o , ( { <. (/) , J >. , <. 1o , K >. } ` 1o ) >. } = { <. 1o , K >. } )`
121 116 120 eqtrd
` |-  ( ph -> ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) = { <. 1o , K >. } )`
122 121 fveq2d
` |-  ( ph -> ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) = ( Xt_ ` { <. 1o , K >. } ) )`
123 122 unieqd
` |-  ( ph -> U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) = U. ( Xt_ ` { <. 1o , K >. } ) )`
124 eqidd
` |-  ( ph -> ( x u. y ) = ( x u. y ) )`
125 111 123 124 mpoeq123dv
` |-  ( ph -> ( x e. U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) , y e. U. ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) |-> ( x u. y ) ) = ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) ) )`
126 110 122 oveq12d
` |-  ( ph -> ( ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) tX ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) ) = ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) )`
127 126 oveq1d
` |-  ( ph -> ( ( ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { (/) } ) ) tX ( Xt_ ` ( { <. (/) , J >. , <. 1o , K >. } |` { 1o } ) ) ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) = ( ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) )`
128 98 125 127 3eltr3d
` |-  ( ph -> ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) ) e. ( ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) )`
129 hmeoco
` |-  ( ( ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) e. ( ( J tX K ) Homeo ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) ) /\ ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) ) e. ( ( ( Xt_ ` { <. (/) , J >. } ) tX ( Xt_ ` { <. 1o , K >. } ) ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) ) -> ( ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) ) o. ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) ) e. ( ( J tX K ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) )`
130 49 128 129 syl2anc
` |-  ( ph -> ( ( x e. U. ( Xt_ ` { <. (/) , J >. } ) , y e. U. ( Xt_ ` { <. 1o , K >. } ) |-> ( x u. y ) ) o. ( x e. X , y e. Y |-> <. { <. (/) , x >. } , { <. 1o , y >. } >. ) ) e. ( ( J tX K ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) )`
131 75 130 eqeltrd
` |-  ( ph -> F e. ( ( J tX K ) Homeo ( Xt_ ` { <. (/) , J >. , <. 1o , K >. } ) ) )`