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 X , y Y x 1 𝑜 y
xpstopnlem1.j φ J TopOn X
xpstopnlem1.k φ K TopOn Y
Assertion xpstopnlem1 φ F J × t K Homeo 𝑡 J 1 𝑜 K

Proof

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