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 = K
ptunhmeo.y Y = L
ptunhmeo.j J = 𝑡 F
ptunhmeo.k K = 𝑡 F A
ptunhmeo.l L = 𝑡 F B
ptunhmeo.g G = x X , y Y x y
ptunhmeo.c φ C V
ptunhmeo.f φ F : C Top
ptunhmeo.u φ C = A B
ptunhmeo.i φ A B =
Assertion ptuncnv φ G -1 = z J z A z B

Proof

Step Hyp Ref Expression
1 ptunhmeo.x X = K
2 ptunhmeo.y Y = L
3 ptunhmeo.j J = 𝑡 F
4 ptunhmeo.k K = 𝑡 F A
5 ptunhmeo.l L = 𝑡 F B
6 ptunhmeo.g G = x X , y Y x y
7 ptunhmeo.c φ C V
8 ptunhmeo.f φ F : C Top
9 ptunhmeo.u φ C = A B
10 ptunhmeo.i φ A B =
11 vex x V
12 vex y V
13 11 12 op1std w = x y 1 st w = x
14 11 12 op2ndd w = x y 2 nd w = y
15 13 14 uneq12d w = x y 1 st w 2 nd w = x y
16 15 mpompt w X × Y 1 st w 2 nd w = x X , y Y x y
17 6 16 eqtr4i G = w X × Y 1 st w 2 nd w
18 xp1st w X × Y 1 st w X
19 18 adantl φ w X × Y 1 st w X
20 ixpeq2 k A F A k = F k k A F A k = k A F k
21 fvres k A F A k = F k
22 21 unieqd k A F A k = F k
23 20 22 mprg k A F A k = k A F k
24 ssun1 A A B
25 24 9 sseqtrrid φ A C
26 7 25 ssexd φ A V
27 8 25 fssresd φ F A : A Top
28 4 ptuni A V F A : A Top k A F A k = K
29 26 27 28 syl2anc φ k A F A k = K
30 23 29 eqtr3id φ k A F k = K
31 30 1 eqtr4di φ k A F k = X
32 31 adantr φ w X × Y k A F k = X
33 19 32 eleqtrrd φ w X × Y 1 st w k A F k
34 xp2nd w X × Y 2 nd w Y
35 34 adantl φ w X × Y 2 nd w Y
36 9 eqcomd φ A B = C
37 uneqdifeq A C A B = A B = C C A = B
38 25 10 37 syl2anc φ A B = C C A = B
39 36 38 mpbid φ C A = B
40 39 ixpeq1d φ k C A F k = k B F k
41 ixpeq2 k B F B k = F k k B F B k = k B F k
42 fvres k B F B k = F k
43 42 unieqd k B F B k = F k
44 41 43 mprg k B F B k = k B F k
45 ssun2 B A B
46 45 9 sseqtrrid φ B C
47 7 46 ssexd φ B V
48 8 46 fssresd φ F B : B Top
49 5 ptuni B V F B : B Top k B F B k = L
50 47 48 49 syl2anc φ k B F B k = L
51 44 50 eqtr3id φ k B F k = L
52 51 2 eqtr4di φ k B F k = Y
53 40 52 eqtrd φ k C A F k = Y
54 53 adantr φ w X × Y k C A F k = Y
55 35 54 eleqtrrd φ w X × Y 2 nd w k C A F k
56 25 adantr φ w X × Y A C
57 undifixp 1 st w k A F k 2 nd w k C A F k A C 1 st w 2 nd w k C F k
58 33 55 56 57 syl3anc φ w X × Y 1 st w 2 nd w k C F k
59 3 ptuni C V F : C Top k C F k = J
60 7 8 59 syl2anc φ k C F k = J
61 60 adantr φ w X × Y k C F k = J
62 58 61 eleqtrd φ w X × Y 1 st w 2 nd w J
63 25 adantr φ z J A C
64 60 eleq2d φ z k C F k z J
65 64 biimpar φ z J z k C F k
66 resixp A C z k C F k z A k A F k
67 63 65 66 syl2anc φ z J z A k A F k
68 31 adantr φ z J k A F k = X
69 67 68 eleqtrd φ z J z A X
70 46 adantr φ z J B C
71 resixp B C z k C F k z B k B F k
72 70 65 71 syl2anc φ z J z B k B F k
73 52 adantr φ z J k B F k = Y
74 72 73 eleqtrd φ z J z B Y
75 69 74 opelxpd φ z J z A z B X × Y
76 eqop w X × Y w = z A z B 1 st w = z A 2 nd w = z B
77 76 ad2antrl φ w X × Y z J w = z A z B 1 st w = z A 2 nd w = z B
78 65 adantrl φ w X × Y z J z k C F k
79 ixpfn z k C F k z Fn C
80 fnresdm z Fn C z C = z
81 78 79 80 3syl φ w X × Y z J z C = z
82 9 reseq2d φ z C = z A B
83 82 adantr φ w X × Y z J z C = z A B
84 81 83 eqtr3d φ w X × Y z J z = z A B
85 resundi z A B = z A z B
86 84 85 eqtrdi φ w X × Y z J z = z A z B
87 uneq12 1 st w = z A 2 nd w = z B 1 st w 2 nd w = z A z B
88 87 eqeq2d 1 st w = z A 2 nd w = z B z = 1 st w 2 nd w z = z A z B
89 86 88 syl5ibrcom φ w X × Y z J 1 st w = z A 2 nd w = z B z = 1 st w 2 nd w
90 ixpfn 1 st w k A F k 1 st w Fn A
91 33 90 syl φ w X × Y 1 st w Fn A
92 91 adantrr φ w X × Y z J 1 st w Fn A
93 dffn2 1 st w Fn A 1 st w : A V
94 92 93 sylib φ w X × Y z J 1 st w : A V
95 52 adantr φ w X × Y k B F k = Y
96 35 95 eleqtrrd φ w X × Y 2 nd w k B F k
97 ixpfn 2 nd w k B F k 2 nd w Fn B
98 96 97 syl φ w X × Y 2 nd w Fn B
99 98 adantrr φ w X × Y z J 2 nd w Fn B
100 dffn2 2 nd w Fn B 2 nd w : B V
101 99 100 sylib φ w X × Y z J 2 nd w : B V
102 res0 1 st w =
103 res0 2 nd w =
104 102 103 eqtr4i 1 st w = 2 nd w
105 10 adantr φ w X × Y z J A B =
106 105 reseq2d φ w X × Y z J 1 st w A B = 1 st w
107 105 reseq2d φ w X × Y z J 2 nd w A B = 2 nd w
108 104 106 107 3eqtr4a φ w X × Y z J 1 st w A B = 2 nd w A B
109 fresaunres1 1 st w : A V 2 nd w : B V 1 st w A B = 2 nd w A B 1 st w 2 nd w A = 1 st w
110 94 101 108 109 syl3anc φ w X × Y z J 1 st w 2 nd w A = 1 st w
111 110 eqcomd φ w X × Y z J 1 st w = 1 st w 2 nd w A
112 fresaunres2 1 st w : A V 2 nd w : B V 1 st w A B = 2 nd w A B 1 st w 2 nd w B = 2 nd w
113 94 101 108 112 syl3anc φ w X × Y z J 1 st w 2 nd w B = 2 nd w
114 113 eqcomd φ w X × Y z J 2 nd w = 1 st w 2 nd w B
115 111 114 jca φ w X × Y z J 1 st w = 1 st w 2 nd w A 2 nd w = 1 st w 2 nd w B
116 reseq1 z = 1 st w 2 nd w z A = 1 st w 2 nd w A
117 116 eqeq2d z = 1 st w 2 nd w 1 st w = z A 1 st w = 1 st w 2 nd w A
118 reseq1 z = 1 st w 2 nd w z B = 1 st w 2 nd w B
119 118 eqeq2d z = 1 st w 2 nd w 2 nd w = z B 2 nd w = 1 st w 2 nd w B
120 117 119 anbi12d z = 1 st w 2 nd w 1 st w = z A 2 nd w = z B 1 st w = 1 st w 2 nd w A 2 nd w = 1 st w 2 nd w B
121 115 120 syl5ibrcom φ w X × Y z J z = 1 st w 2 nd w 1 st w = z A 2 nd w = z B
122 89 121 impbid φ w X × Y z J 1 st w = z A 2 nd w = z B z = 1 st w 2 nd w
123 77 122 bitrd φ w X × Y z J w = z A z B z = 1 st w 2 nd w
124 17 62 75 123 f1ocnv2d φ G : X × Y 1-1 onto J G -1 = z J z A z B
125 124 simprd φ G -1 = z J z A z B