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 eqtr3id 
 |-  ( 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 >. } ) ) )