# Metamath Proof Explorer

## Theorem ptunhmeo

Description: Define a homeomorphism from a binary product of indexed product topologies to an indexed product topology on the union of the index sets. This is the topological analogue of ( A ^ B ) x. ( A ^ C ) = A ^ ( B + C ) . (Contributed by Mario Carneiro, 8-Feb-2015) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses ptunhmeo.x
`|- X = U. K`
ptunhmeo.y
`|- Y = U. L`
ptunhmeo.j
`|- J = ( Xt_ ` F )`
ptunhmeo.k
`|- K = ( Xt_ ` ( F |` A ) )`
ptunhmeo.l
`|- L = ( Xt_ ` ( F |` B ) )`
ptunhmeo.g
`|- G = ( x e. X , y e. Y |-> ( x u. y ) )`
ptunhmeo.c
`|- ( ph -> C e. V )`
ptunhmeo.f
`|- ( ph -> F : C --> Top )`
ptunhmeo.u
`|- ( ph -> C = ( A u. B ) )`
ptunhmeo.i
`|- ( ph -> ( A i^i B ) = (/) )`
Assertion ptunhmeo
`|- ( ph -> G e. ( ( K tX L ) Homeo J ) )`

### Proof

Step Hyp Ref Expression
1 ptunhmeo.x
` |-  X = U. K`
2 ptunhmeo.y
` |-  Y = U. L`
3 ptunhmeo.j
` |-  J = ( Xt_ ` F )`
4 ptunhmeo.k
` |-  K = ( Xt_ ` ( F |` A ) )`
5 ptunhmeo.l
` |-  L = ( Xt_ ` ( F |` B ) )`
6 ptunhmeo.g
` |-  G = ( x e. X , y e. Y |-> ( x u. y ) )`
7 ptunhmeo.c
` |-  ( ph -> C e. V )`
8 ptunhmeo.f
` |-  ( ph -> F : C --> Top )`
9 ptunhmeo.u
` |-  ( ph -> C = ( A u. B ) )`
10 ptunhmeo.i
` |-  ( ph -> ( A i^i B ) = (/) )`
11 vex
` |-  x e. _V`
12 vex
` |-  y e. _V`
13 11 12 op1std
` |-  ( z = <. x , y >. -> ( 1st ` z ) = x )`
14 11 12 op2ndd
` |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )`
15 13 14 uneq12d
` |-  ( z = <. x , y >. -> ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( x u. y ) )`
16 15 mpompt
` |-  ( z e. ( X X. Y ) |-> ( ( 1st ` z ) u. ( 2nd ` z ) ) ) = ( x e. X , y e. Y |-> ( x u. y ) )`
17 6 16 eqtr4i
` |-  G = ( z e. ( X X. Y ) |-> ( ( 1st ` z ) u. ( 2nd ` z ) ) )`
18 xp1st
` |-  ( z e. ( X X. Y ) -> ( 1st ` z ) e. X )`
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( 1st ` z ) e. X )`
20 ixpeq2
` |-  ( A. n e. A U. ( ( F |` A ) ` n ) = U. ( F ` n ) -> X_ n e. A U. ( ( F |` A ) ` n ) = X_ n e. A U. ( F ` n ) )`
21 fvres
` |-  ( n e. A -> ( ( F |` A ) ` n ) = ( F ` n ) )`
22 21 unieqd
` |-  ( n e. A -> U. ( ( F |` A ) ` n ) = U. ( F ` n ) )`
23 20 22 mprg
` |-  X_ n e. A U. ( ( F |` A ) ` n ) = X_ n e. A U. ( F ` n )`
24 ssun1
` |-  A C_ ( A u. B )`
25 24 9 sseqtrrid
` |-  ( ph -> A C_ C )`
26 7 25 ssexd
` |-  ( ph -> A e. _V )`
27 8 25 fssresd
` |-  ( ph -> ( F |` A ) : A --> Top )`
28 4 ptuni
` |-  ( ( A e. _V /\ ( F |` A ) : A --> Top ) -> X_ n e. A U. ( ( F |` A ) ` n ) = U. K )`
29 26 27 28 syl2anc
` |-  ( ph -> X_ n e. A U. ( ( F |` A ) ` n ) = U. K )`
30 23 29 syl5eqr
` |-  ( ph -> X_ n e. A U. ( F ` n ) = U. K )`
31 30 1 eqtr4di
` |-  ( ph -> X_ n e. A U. ( F ` n ) = X )`
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> X_ n e. A U. ( F ` n ) = X )`
33 19 32 eleqtrrd
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( 1st ` z ) e. X_ n e. A U. ( F ` n ) )`
34 xp2nd
` |-  ( z e. ( X X. Y ) -> ( 2nd ` z ) e. Y )`
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( 2nd ` z ) e. Y )`
36 9 eqcomd
` |-  ( ph -> ( A u. B ) = C )`
37 uneqdifeq
` |-  ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C <-> ( C \ A ) = B ) )`
38 25 10 37 syl2anc
` |-  ( ph -> ( ( A u. B ) = C <-> ( C \ A ) = B ) )`
39 36 38 mpbid
` |-  ( ph -> ( C \ A ) = B )`
40 39 ixpeq1d
` |-  ( ph -> X_ n e. ( C \ A ) U. ( F ` n ) = X_ n e. B U. ( F ` n ) )`
41 ixpeq2
` |-  ( A. n e. B U. ( ( F |` B ) ` n ) = U. ( F ` n ) -> X_ n e. B U. ( ( F |` B ) ` n ) = X_ n e. B U. ( F ` n ) )`
42 fvres
` |-  ( n e. B -> ( ( F |` B ) ` n ) = ( F ` n ) )`
43 42 unieqd
` |-  ( n e. B -> U. ( ( F |` B ) ` n ) = U. ( F ` n ) )`
44 41 43 mprg
` |-  X_ n e. B U. ( ( F |` B ) ` n ) = X_ n e. B U. ( F ` n )`
45 ssun2
` |-  B C_ ( A u. B )`
46 45 9 sseqtrrid
` |-  ( ph -> B C_ C )`
47 7 46 ssexd
` |-  ( ph -> B e. _V )`
48 8 46 fssresd
` |-  ( ph -> ( F |` B ) : B --> Top )`
49 5 ptuni
` |-  ( ( B e. _V /\ ( F |` B ) : B --> Top ) -> X_ n e. B U. ( ( F |` B ) ` n ) = U. L )`
50 47 48 49 syl2anc
` |-  ( ph -> X_ n e. B U. ( ( F |` B ) ` n ) = U. L )`
51 44 50 syl5eqr
` |-  ( ph -> X_ n e. B U. ( F ` n ) = U. L )`
52 51 2 eqtr4di
` |-  ( ph -> X_ n e. B U. ( F ` n ) = Y )`
53 40 52 eqtrd
` |-  ( ph -> X_ n e. ( C \ A ) U. ( F ` n ) = Y )`
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> X_ n e. ( C \ A ) U. ( F ` n ) = Y )`
55 35 54 eleqtrrd
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( 2nd ` z ) e. X_ n e. ( C \ A ) U. ( F ` n ) )`
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> A C_ C )`
57 undifixp
` |-  ( ( ( 1st ` z ) e. X_ n e. A U. ( F ` n ) /\ ( 2nd ` z ) e. X_ n e. ( C \ A ) U. ( F ` n ) /\ A C_ C ) -> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. X_ n e. C U. ( F ` n ) )`
58 33 55 56 57 syl3anc
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( ( 1st ` z ) u. ( 2nd ` z ) ) e. X_ n e. C U. ( F ` n ) )`
59 ixpfn
` |-  ( ( ( 1st ` z ) u. ( 2nd ` z ) ) e. X_ n e. C U. ( F ` n ) -> ( ( 1st ` z ) u. ( 2nd ` z ) ) Fn C )`
60 58 59 syl
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( ( 1st ` z ) u. ( 2nd ` z ) ) Fn C )`
61 dffn5
` |-  ( ( ( 1st ` z ) u. ( 2nd ` z ) ) Fn C <-> ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( k e. C |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) )`
62 60 61 sylib
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( ( 1st ` z ) u. ( 2nd ` z ) ) = ( k e. C |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) )`
63 62 mpteq2dva
` |-  ( ph -> ( z e. ( X X. Y ) |-> ( ( 1st ` z ) u. ( 2nd ` z ) ) ) = ( z e. ( X X. Y ) |-> ( k e. C |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) ) )`
64 17 63 syl5eq
` |-  ( ph -> G = ( z e. ( X X. Y ) |-> ( k e. C |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) ) )`
65 pttop
` |-  ( ( A e. _V /\ ( F |` A ) : A --> Top ) -> ( Xt_ ` ( F |` A ) ) e. Top )`
66 26 27 65 syl2anc
` |-  ( ph -> ( Xt_ ` ( F |` A ) ) e. Top )`
67 4 66 eqeltrid
` |-  ( ph -> K e. Top )`
68 1 toptopon
` |-  ( K e. Top <-> K e. ( TopOn ` X ) )`
69 67 68 sylib
` |-  ( ph -> K e. ( TopOn ` X ) )`
70 pttop
` |-  ( ( B e. _V /\ ( F |` B ) : B --> Top ) -> ( Xt_ ` ( F |` B ) ) e. Top )`
71 47 48 70 syl2anc
` |-  ( ph -> ( Xt_ ` ( F |` B ) ) e. Top )`
72 5 71 eqeltrid
` |-  ( ph -> L e. Top )`
73 2 toptopon
` |-  ( L e. Top <-> L e. ( TopOn ` Y ) )`
74 72 73 sylib
` |-  ( ph -> L e. ( TopOn ` Y ) )`
75 txtopon
` |-  ( ( K e. ( TopOn ` X ) /\ L e. ( TopOn ` Y ) ) -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )`
76 69 74 75 syl2anc
` |-  ( ph -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )`
77 9 eleq2d
` |-  ( ph -> ( k e. C <-> k e. ( A u. B ) ) )`
78 77 biimpa
` |-  ( ( ph /\ k e. C ) -> k e. ( A u. B ) )`
79 elun
` |-  ( k e. ( A u. B ) <-> ( k e. A \/ k e. B ) )`
80 78 79 sylib
` |-  ( ( ph /\ k e. C ) -> ( k e. A \/ k e. B ) )`
81 ixpfn
` |-  ( ( 1st ` z ) e. X_ n e. A U. ( F ` n ) -> ( 1st ` z ) Fn A )`
82 33 81 syl
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( 1st ` z ) Fn A )`
` |-  ( ( ( ph /\ k e. A ) /\ z e. ( X X. Y ) ) -> ( 1st ` z ) Fn A )`
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> X_ n e. B U. ( F ` n ) = Y )`
85 35 84 eleqtrrd
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( 2nd ` z ) e. X_ n e. B U. ( F ` n ) )`
86 ixpfn
` |-  ( ( 2nd ` z ) e. X_ n e. B U. ( F ` n ) -> ( 2nd ` z ) Fn B )`
87 85 86 syl
` |-  ( ( ph /\ z e. ( X X. Y ) ) -> ( 2nd ` z ) Fn B )`
` |-  ( ( ( ph /\ k e. A ) /\ z e. ( X X. Y ) ) -> ( 2nd ` z ) Fn B )`
` |-  ( ( ( ph /\ k e. A ) /\ z e. ( X X. Y ) ) -> ( A i^i B ) = (/) )`
90 simplr
` |-  ( ( ( ph /\ k e. A ) /\ z e. ( X X. Y ) ) -> k e. A )`
91 fvun1
` |-  ( ( ( 1st ` z ) Fn A /\ ( 2nd ` z ) Fn B /\ ( ( A i^i B ) = (/) /\ k e. A ) ) -> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) = ( ( 1st ` z ) ` k ) )`
92 83 88 89 90 91 syl112anc
` |-  ( ( ( ph /\ k e. A ) /\ z e. ( X X. Y ) ) -> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) = ( ( 1st ` z ) ` k ) )`
93 92 mpteq2dva
` |-  ( ( ph /\ k e. A ) -> ( z e. ( X X. Y ) |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) = ( z e. ( X X. Y ) |-> ( ( 1st ` z ) ` k ) ) )`
` |-  ( ( ph /\ k e. A ) -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )`
95 13 mpompt
` |-  ( z e. ( X X. Y ) |-> ( 1st ` z ) ) = ( x e. X , y e. Y |-> x )`
` |-  ( ( ph /\ k e. A ) -> K e. ( TopOn ` X ) )`
` |-  ( ( ph /\ k e. A ) -> L e. ( TopOn ` Y ) )`
98 96 97 cnmpt1st
` |-  ( ( ph /\ k e. A ) -> ( x e. X , y e. Y |-> x ) e. ( ( K tX L ) Cn K ) )`
99 95 98 eqeltrid
` |-  ( ( ph /\ k e. A ) -> ( z e. ( X X. Y ) |-> ( 1st ` z ) ) e. ( ( K tX L ) Cn K ) )`
` |-  ( ( ph /\ k e. A ) -> A e. _V )`
` |-  ( ( ph /\ k e. A ) -> ( F |` A ) : A --> Top )`
102 simpr
` |-  ( ( ph /\ k e. A ) -> k e. A )`
103 1 4 ptpjcn
` |-  ( ( A e. _V /\ ( F |` A ) : A --> Top /\ k e. A ) -> ( f e. X |-> ( f ` k ) ) e. ( K Cn ( ( F |` A ) ` k ) ) )`
104 100 101 102 103 syl3anc
` |-  ( ( ph /\ k e. A ) -> ( f e. X |-> ( f ` k ) ) e. ( K Cn ( ( F |` A ) ` k ) ) )`
105 fvres
` |-  ( k e. A -> ( ( F |` A ) ` k ) = ( F ` k ) )`
` |-  ( ( ph /\ k e. A ) -> ( ( F |` A ) ` k ) = ( F ` k ) )`
107 106 oveq2d
` |-  ( ( ph /\ k e. A ) -> ( K Cn ( ( F |` A ) ` k ) ) = ( K Cn ( F ` k ) ) )`
108 104 107 eleqtrd
` |-  ( ( ph /\ k e. A ) -> ( f e. X |-> ( f ` k ) ) e. ( K Cn ( F ` k ) ) )`
109 fveq1
` |-  ( f = ( 1st ` z ) -> ( f ` k ) = ( ( 1st ` z ) ` k ) )`
110 94 99 96 108 109 cnmpt11
` |-  ( ( ph /\ k e. A ) -> ( z e. ( X X. Y ) |-> ( ( 1st ` z ) ` k ) ) e. ( ( K tX L ) Cn ( F ` k ) ) )`
111 93 110 eqeltrd
` |-  ( ( ph /\ k e. A ) -> ( z e. ( X X. Y ) |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) e. ( ( K tX L ) Cn ( F ` k ) ) )`
` |-  ( ( ( ph /\ k e. B ) /\ z e. ( X X. Y ) ) -> ( 1st ` z ) Fn A )`
` |-  ( ( ( ph /\ k e. B ) /\ z e. ( X X. Y ) ) -> ( 2nd ` z ) Fn B )`
` |-  ( ( ( ph /\ k e. B ) /\ z e. ( X X. Y ) ) -> ( A i^i B ) = (/) )`
115 simplr
` |-  ( ( ( ph /\ k e. B ) /\ z e. ( X X. Y ) ) -> k e. B )`
116 fvun2
` |-  ( ( ( 1st ` z ) Fn A /\ ( 2nd ` z ) Fn B /\ ( ( A i^i B ) = (/) /\ k e. B ) ) -> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) = ( ( 2nd ` z ) ` k ) )`
117 112 113 114 115 116 syl112anc
` |-  ( ( ( ph /\ k e. B ) /\ z e. ( X X. Y ) ) -> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) = ( ( 2nd ` z ) ` k ) )`
118 117 mpteq2dva
` |-  ( ( ph /\ k e. B ) -> ( z e. ( X X. Y ) |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) = ( z e. ( X X. Y ) |-> ( ( 2nd ` z ) ` k ) ) )`
` |-  ( ( ph /\ k e. B ) -> ( K tX L ) e. ( TopOn ` ( X X. Y ) ) )`
120 14 mpompt
` |-  ( z e. ( X X. Y ) |-> ( 2nd ` z ) ) = ( x e. X , y e. Y |-> y )`
` |-  ( ( ph /\ k e. B ) -> K e. ( TopOn ` X ) )`
` |-  ( ( ph /\ k e. B ) -> L e. ( TopOn ` Y ) )`
123 121 122 cnmpt2nd
` |-  ( ( ph /\ k e. B ) -> ( x e. X , y e. Y |-> y ) e. ( ( K tX L ) Cn L ) )`
124 120 123 eqeltrid
` |-  ( ( ph /\ k e. B ) -> ( z e. ( X X. Y ) |-> ( 2nd ` z ) ) e. ( ( K tX L ) Cn L ) )`
` |-  ( ( ph /\ k e. B ) -> B e. _V )`
` |-  ( ( ph /\ k e. B ) -> ( F |` B ) : B --> Top )`
127 simpr
` |-  ( ( ph /\ k e. B ) -> k e. B )`
128 2 5 ptpjcn
` |-  ( ( B e. _V /\ ( F |` B ) : B --> Top /\ k e. B ) -> ( f e. Y |-> ( f ` k ) ) e. ( L Cn ( ( F |` B ) ` k ) ) )`
129 125 126 127 128 syl3anc
` |-  ( ( ph /\ k e. B ) -> ( f e. Y |-> ( f ` k ) ) e. ( L Cn ( ( F |` B ) ` k ) ) )`
130 fvres
` |-  ( k e. B -> ( ( F |` B ) ` k ) = ( F ` k ) )`
` |-  ( ( ph /\ k e. B ) -> ( ( F |` B ) ` k ) = ( F ` k ) )`
132 131 oveq2d
` |-  ( ( ph /\ k e. B ) -> ( L Cn ( ( F |` B ) ` k ) ) = ( L Cn ( F ` k ) ) )`
133 129 132 eleqtrd
` |-  ( ( ph /\ k e. B ) -> ( f e. Y |-> ( f ` k ) ) e. ( L Cn ( F ` k ) ) )`
134 fveq1
` |-  ( f = ( 2nd ` z ) -> ( f ` k ) = ( ( 2nd ` z ) ` k ) )`
135 119 124 122 133 134 cnmpt11
` |-  ( ( ph /\ k e. B ) -> ( z e. ( X X. Y ) |-> ( ( 2nd ` z ) ` k ) ) e. ( ( K tX L ) Cn ( F ` k ) ) )`
136 118 135 eqeltrd
` |-  ( ( ph /\ k e. B ) -> ( z e. ( X X. Y ) |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) e. ( ( K tX L ) Cn ( F ` k ) ) )`
137 111 136 jaodan
` |-  ( ( ph /\ ( k e. A \/ k e. B ) ) -> ( z e. ( X X. Y ) |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) e. ( ( K tX L ) Cn ( F ` k ) ) )`
138 80 137 syldan
` |-  ( ( ph /\ k e. C ) -> ( z e. ( X X. Y ) |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) e. ( ( K tX L ) Cn ( F ` k ) ) )`
139 3 76 7 8 138 ptcn
` |-  ( ph -> ( z e. ( X X. Y ) |-> ( k e. C |-> ( ( ( 1st ` z ) u. ( 2nd ` z ) ) ` k ) ) ) e. ( ( K tX L ) Cn J ) )`
140 64 139 eqeltrd
` |-  ( ph -> G e. ( ( K tX L ) Cn J ) )`
141 1 2 3 4 5 6 7 8 9 10 ptuncnv
` |-  ( ph -> `' G = ( z e. U. J |-> <. ( z |` A ) , ( z |` B ) >. ) )`
142 pttop
` |-  ( ( C e. V /\ F : C --> Top ) -> ( Xt_ ` F ) e. Top )`
143 7 8 142 syl2anc
` |-  ( ph -> ( Xt_ ` F ) e. Top )`
144 3 143 eqeltrid
` |-  ( ph -> J e. Top )`
145 eqid
` |-  U. J = U. J`
146 145 toptopon
` |-  ( J e. Top <-> J e. ( TopOn ` U. J ) )`
147 144 146 sylib
` |-  ( ph -> J e. ( TopOn ` U. J ) )`
148 145 3 4 ptrescn
` |-  ( ( C e. V /\ F : C --> Top /\ A C_ C ) -> ( z e. U. J |-> ( z |` A ) ) e. ( J Cn K ) )`
149 7 8 25 148 syl3anc
` |-  ( ph -> ( z e. U. J |-> ( z |` A ) ) e. ( J Cn K ) )`
150 145 3 5 ptrescn
` |-  ( ( C e. V /\ F : C --> Top /\ B C_ C ) -> ( z e. U. J |-> ( z |` B ) ) e. ( J Cn L ) )`
151 7 8 46 150 syl3anc
` |-  ( ph -> ( z e. U. J |-> ( z |` B ) ) e. ( J Cn L ) )`
152 147 149 151 cnmpt1t
` |-  ( ph -> ( z e. U. J |-> <. ( z |` A ) , ( z |` B ) >. ) e. ( J Cn ( K tX L ) ) )`
153 141 152 eqeltrd
` |-  ( ph -> `' G e. ( J Cn ( K tX L ) ) )`
154 ishmeo
` |-  ( G e. ( ( K tX L ) Homeo J ) <-> ( G e. ( ( K tX L ) Cn J ) /\ `' G e. ( J Cn ( K tX L ) ) ) )`
155 140 153 154 sylanbrc
` |-  ( ph -> G e. ( ( K tX L ) Homeo J ) )`