# Metamath Proof Explorer

## Theorem ptuncnv

Description: Exhibit the converse function of the map G which joins two product topologies on disjoint index sets. (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 ptuncnv
`|- ( ph -> `' G = ( z e. U. J |-> <. ( z |` A ) , ( z |` B ) >. ) )`

### 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
` |-  ( w = <. x , y >. -> ( 1st ` w ) = x )`
14 11 12 op2ndd
` |-  ( w = <. x , y >. -> ( 2nd ` w ) = y )`
15 13 14 uneq12d
` |-  ( w = <. x , y >. -> ( ( 1st ` w ) u. ( 2nd ` w ) ) = ( x u. y ) )`
16 15 mpompt
` |-  ( w e. ( X X. Y ) |-> ( ( 1st ` w ) u. ( 2nd ` w ) ) ) = ( x e. X , y e. Y |-> ( x u. y ) )`
17 6 16 eqtr4i
` |-  G = ( w e. ( X X. Y ) |-> ( ( 1st ` w ) u. ( 2nd ` w ) ) )`
18 xp1st
` |-  ( w e. ( X X. Y ) -> ( 1st ` w ) e. X )`
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> ( 1st ` w ) e. X )`
20 ixpeq2
` |-  ( A. k e. A U. ( ( F |` A ) ` k ) = U. ( F ` k ) -> X_ k e. A U. ( ( F |` A ) ` k ) = X_ k e. A U. ( F ` k ) )`
21 fvres
` |-  ( k e. A -> ( ( F |` A ) ` k ) = ( F ` k ) )`
22 21 unieqd
` |-  ( k e. A -> U. ( ( F |` A ) ` k ) = U. ( F ` k ) )`
23 20 22 mprg
` |-  X_ k e. A U. ( ( F |` A ) ` k ) = X_ k e. A U. ( F ` k )`
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_ k e. A U. ( ( F |` A ) ` k ) = U. K )`
29 26 27 28 syl2anc
` |-  ( ph -> X_ k e. A U. ( ( F |` A ) ` k ) = U. K )`
30 23 29 syl5eqr
` |-  ( ph -> X_ k e. A U. ( F ` k ) = U. K )`
31 30 1 eqtr4di
` |-  ( ph -> X_ k e. A U. ( F ` k ) = X )`
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> X_ k e. A U. ( F ` k ) = X )`
33 19 32 eleqtrrd
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> ( 1st ` w ) e. X_ k e. A U. ( F ` k ) )`
34 xp2nd
` |-  ( w e. ( X X. Y ) -> ( 2nd ` w ) e. Y )`
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> ( 2nd ` w ) 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_ k e. ( C \ A ) U. ( F ` k ) = X_ k e. B U. ( F ` k ) )`
41 ixpeq2
` |-  ( A. k e. B U. ( ( F |` B ) ` k ) = U. ( F ` k ) -> X_ k e. B U. ( ( F |` B ) ` k ) = X_ k e. B U. ( F ` k ) )`
42 fvres
` |-  ( k e. B -> ( ( F |` B ) ` k ) = ( F ` k ) )`
43 42 unieqd
` |-  ( k e. B -> U. ( ( F |` B ) ` k ) = U. ( F ` k ) )`
44 41 43 mprg
` |-  X_ k e. B U. ( ( F |` B ) ` k ) = X_ k e. B U. ( F ` k )`
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_ k e. B U. ( ( F |` B ) ` k ) = U. L )`
50 47 48 49 syl2anc
` |-  ( ph -> X_ k e. B U. ( ( F |` B ) ` k ) = U. L )`
51 44 50 syl5eqr
` |-  ( ph -> X_ k e. B U. ( F ` k ) = U. L )`
52 51 2 eqtr4di
` |-  ( ph -> X_ k e. B U. ( F ` k ) = Y )`
53 40 52 eqtrd
` |-  ( ph -> X_ k e. ( C \ A ) U. ( F ` k ) = Y )`
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> X_ k e. ( C \ A ) U. ( F ` k ) = Y )`
55 35 54 eleqtrrd
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> ( 2nd ` w ) e. X_ k e. ( C \ A ) U. ( F ` k ) )`
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> A C_ C )`
57 undifixp
` |-  ( ( ( 1st ` w ) e. X_ k e. A U. ( F ` k ) /\ ( 2nd ` w ) e. X_ k e. ( C \ A ) U. ( F ` k ) /\ A C_ C ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. X_ k e. C U. ( F ` k ) )`
58 33 55 56 57 syl3anc
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. X_ k e. C U. ( F ` k ) )`
59 3 ptuni
` |-  ( ( C e. V /\ F : C --> Top ) -> X_ k e. C U. ( F ` k ) = U. J )`
60 7 8 59 syl2anc
` |-  ( ph -> X_ k e. C U. ( F ` k ) = U. J )`
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> X_ k e. C U. ( F ` k ) = U. J )`
62 58 61 eleqtrd
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) e. U. J )`
` |-  ( ( ph /\ z e. U. J ) -> A C_ C )`
64 60 eleq2d
` |-  ( ph -> ( z e. X_ k e. C U. ( F ` k ) <-> z e. U. J ) )`
65 64 biimpar
` |-  ( ( ph /\ z e. U. J ) -> z e. X_ k e. C U. ( F ` k ) )`
66 resixp
` |-  ( ( A C_ C /\ z e. X_ k e. C U. ( F ` k ) ) -> ( z |` A ) e. X_ k e. A U. ( F ` k ) )`
67 63 65 66 syl2anc
` |-  ( ( ph /\ z e. U. J ) -> ( z |` A ) e. X_ k e. A U. ( F ` k ) )`
` |-  ( ( ph /\ z e. U. J ) -> X_ k e. A U. ( F ` k ) = X )`
69 67 68 eleqtrd
` |-  ( ( ph /\ z e. U. J ) -> ( z |` A ) e. X )`
` |-  ( ( ph /\ z e. U. J ) -> B C_ C )`
71 resixp
` |-  ( ( B C_ C /\ z e. X_ k e. C U. ( F ` k ) ) -> ( z |` B ) e. X_ k e. B U. ( F ` k ) )`
72 70 65 71 syl2anc
` |-  ( ( ph /\ z e. U. J ) -> ( z |` B ) e. X_ k e. B U. ( F ` k ) )`
` |-  ( ( ph /\ z e. U. J ) -> X_ k e. B U. ( F ` k ) = Y )`
74 72 73 eleqtrd
` |-  ( ( ph /\ z e. U. J ) -> ( z |` B ) e. Y )`
75 69 74 opelxpd
` |-  ( ( ph /\ z e. U. J ) -> <. ( z |` A ) , ( z |` B ) >. e. ( X X. Y ) )`
76 eqop
` |-  ( w e. ( X X. Y ) -> ( w = <. ( z |` A ) , ( z |` B ) >. <-> ( ( 1st ` w ) = ( z |` A ) /\ ( 2nd ` w ) = ( z |` B ) ) ) )`
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( w = <. ( z |` A ) , ( z |` B ) >. <-> ( ( 1st ` w ) = ( z |` A ) /\ ( 2nd ` w ) = ( z |` B ) ) ) )`
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> z e. X_ k e. C U. ( F ` k ) )`
79 ixpfn
` |-  ( z e. X_ k e. C U. ( F ` k ) -> z Fn C )`
80 fnresdm
` |-  ( z Fn C -> ( z |` C ) = z )`
81 78 79 80 3syl
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( z |` C ) = z )`
82 9 reseq2d
` |-  ( ph -> ( z |` C ) = ( z |` ( A u. B ) ) )`
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( z |` C ) = ( z |` ( A u. B ) ) )`
84 81 83 eqtr3d
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> z = ( z |` ( A u. B ) ) )`
85 resundi
` |-  ( z |` ( A u. B ) ) = ( ( z |` A ) u. ( z |` B ) )`
86 84 85 eqtrdi
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> z = ( ( z |` A ) u. ( z |` B ) ) )`
87 uneq12
` |-  ( ( ( 1st ` w ) = ( z |` A ) /\ ( 2nd ` w ) = ( z |` B ) ) -> ( ( 1st ` w ) u. ( 2nd ` w ) ) = ( ( z |` A ) u. ( z |` B ) ) )`
88 87 eqeq2d
` |-  ( ( ( 1st ` w ) = ( z |` A ) /\ ( 2nd ` w ) = ( z |` B ) ) -> ( z = ( ( 1st ` w ) u. ( 2nd ` w ) ) <-> z = ( ( z |` A ) u. ( z |` B ) ) ) )`
89 86 88 syl5ibrcom
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( ( ( 1st ` w ) = ( z |` A ) /\ ( 2nd ` w ) = ( z |` B ) ) -> z = ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )`
90 ixpfn
` |-  ( ( 1st ` w ) e. X_ k e. A U. ( F ` k ) -> ( 1st ` w ) Fn A )`
91 33 90 syl
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> ( 1st ` w ) Fn A )`
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( 1st ` w ) Fn A )`
93 dffn2
` |-  ( ( 1st ` w ) Fn A <-> ( 1st ` w ) : A --> _V )`
94 92 93 sylib
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( 1st ` w ) : A --> _V )`
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> X_ k e. B U. ( F ` k ) = Y )`
96 35 95 eleqtrrd
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> ( 2nd ` w ) e. X_ k e. B U. ( F ` k ) )`
97 ixpfn
` |-  ( ( 2nd ` w ) e. X_ k e. B U. ( F ` k ) -> ( 2nd ` w ) Fn B )`
98 96 97 syl
` |-  ( ( ph /\ w e. ( X X. Y ) ) -> ( 2nd ` w ) Fn B )`
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( 2nd ` w ) Fn B )`
100 dffn2
` |-  ( ( 2nd ` w ) Fn B <-> ( 2nd ` w ) : B --> _V )`
101 99 100 sylib
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( 2nd ` w ) : B --> _V )`
102 res0
` |-  ( ( 1st ` w ) |` (/) ) = (/)`
103 res0
` |-  ( ( 2nd ` w ) |` (/) ) = (/)`
104 102 103 eqtr4i
` |-  ( ( 1st ` w ) |` (/) ) = ( ( 2nd ` w ) |` (/) )`
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( A i^i B ) = (/) )`
106 105 reseq2d
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( ( 1st ` w ) |` ( A i^i B ) ) = ( ( 1st ` w ) |` (/) ) )`
107 105 reseq2d
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( ( 2nd ` w ) |` ( A i^i B ) ) = ( ( 2nd ` w ) |` (/) ) )`
108 104 106 107 3eqtr4a
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( ( 1st ` w ) |` ( A i^i B ) ) = ( ( 2nd ` w ) |` ( A i^i B ) ) )`
109 fresaunres1
` |-  ( ( ( 1st ` w ) : A --> _V /\ ( 2nd ` w ) : B --> _V /\ ( ( 1st ` w ) |` ( A i^i B ) ) = ( ( 2nd ` w ) |` ( A i^i B ) ) ) -> ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` A ) = ( 1st ` w ) )`
110 94 101 108 109 syl3anc
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` A ) = ( 1st ` w ) )`
111 110 eqcomd
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( 1st ` w ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` A ) )`
112 fresaunres2
` |-  ( ( ( 1st ` w ) : A --> _V /\ ( 2nd ` w ) : B --> _V /\ ( ( 1st ` w ) |` ( A i^i B ) ) = ( ( 2nd ` w ) |` ( A i^i B ) ) ) -> ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` B ) = ( 2nd ` w ) )`
113 94 101 108 112 syl3anc
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` B ) = ( 2nd ` w ) )`
114 113 eqcomd
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( 2nd ` w ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` B ) )`
115 111 114 jca
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( ( 1st ` w ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` A ) /\ ( 2nd ` w ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` B ) ) )`
116 reseq1
` |-  ( z = ( ( 1st ` w ) u. ( 2nd ` w ) ) -> ( z |` A ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` A ) )`
117 116 eqeq2d
` |-  ( z = ( ( 1st ` w ) u. ( 2nd ` w ) ) -> ( ( 1st ` w ) = ( z |` A ) <-> ( 1st ` w ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` A ) ) )`
118 reseq1
` |-  ( z = ( ( 1st ` w ) u. ( 2nd ` w ) ) -> ( z |` B ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` B ) )`
119 118 eqeq2d
` |-  ( z = ( ( 1st ` w ) u. ( 2nd ` w ) ) -> ( ( 2nd ` w ) = ( z |` B ) <-> ( 2nd ` w ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` B ) ) )`
120 117 119 anbi12d
` |-  ( z = ( ( 1st ` w ) u. ( 2nd ` w ) ) -> ( ( ( 1st ` w ) = ( z |` A ) /\ ( 2nd ` w ) = ( z |` B ) ) <-> ( ( 1st ` w ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` A ) /\ ( 2nd ` w ) = ( ( ( 1st ` w ) u. ( 2nd ` w ) ) |` B ) ) ) )`
121 115 120 syl5ibrcom
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( z = ( ( 1st ` w ) u. ( 2nd ` w ) ) -> ( ( 1st ` w ) = ( z |` A ) /\ ( 2nd ` w ) = ( z |` B ) ) ) )`
122 89 121 impbid
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( ( ( 1st ` w ) = ( z |` A ) /\ ( 2nd ` w ) = ( z |` B ) ) <-> z = ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )`
123 77 122 bitrd
` |-  ( ( ph /\ ( w e. ( X X. Y ) /\ z e. U. J ) ) -> ( w = <. ( z |` A ) , ( z |` B ) >. <-> z = ( ( 1st ` w ) u. ( 2nd ` w ) ) ) )`
124 17 62 75 123 f1ocnv2d
` |-  ( ph -> ( G : ( X X. Y ) -1-1-onto-> U. J /\ `' G = ( z e. U. J |-> <. ( z |` A ) , ( z |` B ) >. ) ) )`
125 124 simprd
` |-  ( ph -> `' G = ( z e. U. J |-> <. ( z |` A ) , ( z |` B ) >. ) )`