Metamath Proof Explorer


Theorem xkoinjcn

Description: Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis xkoinjcn.3 F = x X y Y y x
Assertion xkoinjcn R TopOn X S TopOn Y F R Cn S × t R ^ ko S

Proof

Step Hyp Ref Expression
1 xkoinjcn.3 F = x X y Y y x
2 simplr R TopOn X S TopOn Y x X S TopOn Y
3 2 cnmptid R TopOn X S TopOn Y x X y Y y S Cn S
4 simpll R TopOn X S TopOn Y x X R TopOn X
5 simpr R TopOn X S TopOn Y x X x X
6 2 4 5 cnmptc R TopOn X S TopOn Y x X y Y x S Cn R
7 2 3 6 cnmpt1t R TopOn X S TopOn Y x X y Y y x S Cn S × t R
8 7 1 fmptd R TopOn X S TopOn Y F : X S Cn S × t R
9 eqid S = S
10 eqid w 𝒫 S | S 𝑡 w Comp = w 𝒫 S | S 𝑡 w Comp
11 eqid k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v = k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v
12 9 10 11 xkobval ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v = z | k 𝒫 S v S × t R S 𝑡 k Comp z = f S Cn S × t R | f k v
13 12 abeq2i z ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v k 𝒫 S v S × t R S 𝑡 k Comp z = f S Cn S × t R | f k v
14 simpll R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp R TopOn X S TopOn Y
15 14 7 sylan R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X y Y y x S Cn S × t R
16 imaeq1 f = y Y y x f k = y Y y x k
17 16 sseq1d f = y Y y x f k v y Y y x k v
18 17 elrab3 y Y y x S Cn S × t R y Y y x f S Cn S × t R | f k v y Y y x k v
19 15 18 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X y Y y x f S Cn S × t R | f k v y Y y x k v
20 funmpt Fun y Y y x
21 simplrl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp k 𝒫 S
22 21 elpwid R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp k S
23 14 simprd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp S TopOn Y
24 toponuni S TopOn Y Y = S
25 23 24 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp Y = S
26 22 25 sseqtrrd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp k Y
27 26 adantr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X k Y
28 dmmptg y Y y x V dom y Y y x = Y
29 opex y x V
30 29 a1i y Y y x V
31 28 30 mprg dom y Y y x = Y
32 27 31 sseqtrrdi R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X k dom y Y y x
33 funimass4 Fun y Y y x k dom y Y y x y Y y x k v z k y Y y x z v
34 20 32 33 sylancr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X y Y y x k v z k y Y y x z v
35 27 sselda R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X z k z Y
36 opeq1 y = z y x = z x
37 eqid y Y y x = y Y y x
38 opex z x V
39 36 37 38 fvmpt z Y y Y y x z = z x
40 35 39 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X z k y Y y x z = z x
41 40 eleq1d R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X z k y Y y x z v z x v
42 vex x V
43 opeq2 w = x z w = z x
44 43 eleq1d w = x z w v z x v
45 42 44 ralsn w x z w v z x v
46 41 45 bitr4di R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X z k y Y y x z v w x z w v
47 46 ralbidva R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X z k y Y y x z v z k w x z w v
48 dfss3 k × x v t k × x t v
49 eleq1 t = z w t v z w v
50 49 ralxp t k × x t v z k w x z w v
51 48 50 bitri k × x v z k w x z w v
52 47 51 bitr4di R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X z k y Y y x z v k × x v
53 19 34 52 3bitrd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X y Y y x f S Cn S × t R | f k v k × x v
54 53 rabbidva R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X | y Y y x f S Cn S × t R | f k v = x X | k × x v
55 sneq x = w x = w
56 55 xpeq2d x = w k × x = k × w
57 56 sseq1d x = w k × x v k × w v
58 57 elrab w x X | k × x v w X k × w v
59 eqid S 𝑡 k = S 𝑡 k
60 eqid R = R
61 simplr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v S 𝑡 k Comp
62 simpll R TopOn X S TopOn Y k 𝒫 S v S × t R R TopOn X
63 62 ad2antrr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v R TopOn X
64 topontop R TopOn X R Top
65 63 64 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v R Top
66 topontop S TopOn Y S Top
67 66 adantl R TopOn X S TopOn Y S Top
68 64 adantr R TopOn X S TopOn Y R Top
69 txtop S Top R Top S × t R Top
70 67 68 69 syl2anc R TopOn X S TopOn Y S × t R Top
71 70 ad3antrrr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v S × t R Top
72 vex k V
73 toponmax R TopOn X X R
74 63 73 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v X R
75 xpexg k V X R k × X V
76 72 74 75 sylancr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v k × X V
77 simprr R TopOn X S TopOn Y k 𝒫 S v S × t R v S × t R
78 77 ad2antrr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v v S × t R
79 elrestr S × t R Top k × X V v S × t R v k × X S × t R 𝑡 k × X
80 71 76 78 79 syl3anc R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v v k × X S × t R 𝑡 k × X
81 67 ad3antrrr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v S Top
82 72 a1i R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v k V
83 txrest S Top R Top k V X R S × t R 𝑡 k × X = S 𝑡 k × t R 𝑡 X
84 81 65 82 74 83 syl22anc R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v S × t R 𝑡 k × X = S 𝑡 k × t R 𝑡 X
85 toponuni R TopOn X X = R
86 63 85 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v X = R
87 86 oveq2d R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v R 𝑡 X = R 𝑡 R
88 60 restid R TopOn X R 𝑡 R = R
89 63 88 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v R 𝑡 R = R
90 87 89 eqtrd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v R 𝑡 X = R
91 90 oveq2d R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v S 𝑡 k × t R 𝑡 X = S 𝑡 k × t R
92 84 91 eqtrd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v S × t R 𝑡 k × X = S 𝑡 k × t R
93 80 92 eleqtrd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v v k × X S 𝑡 k × t R
94 23 adantr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v S TopOn Y
95 26 adantr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v k Y
96 resttopon S TopOn Y k Y S 𝑡 k TopOn k
97 94 95 96 syl2anc R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v S 𝑡 k TopOn k
98 toponuni S 𝑡 k TopOn k k = S 𝑡 k
99 97 98 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v k = S 𝑡 k
100 99 xpeq1d R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v k × w = S 𝑡 k × w
101 simprr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v k × w v
102 simprl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v w X
103 102 snssd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v w X
104 xpss2 w X k × w k × X
105 103 104 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v k × w k × X
106 101 105 ssind R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v k × w v k × X
107 100 106 eqsstrrd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v S 𝑡 k × w v k × X
108 102 86 eleqtrd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v w R
109 59 60 61 65 93 107 108 txtube R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R w r S 𝑡 k × r v k × X
110 toponss R TopOn X r R r X
111 63 110 sylan R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R r X
112 ssrab r x X | k × x v r X x r k × x v
113 112 baib r X r x X | k × x v x r k × x v
114 111 113 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R r x X | k × x v x r k × x v
115 xpss2 r X k × r k × X
116 111 115 syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R k × r k × X
117 116 biantrud R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R k × r v k × r v k × r k × X
118 iunid x r x = r
119 118 xpeq2i k × x r x = k × r
120 xpiundi k × x r x = x r k × x
121 119 120 eqtr3i k × r = x r k × x
122 121 sseq1i k × r v x r k × x v
123 iunss x r k × x v x r k × x v
124 122 123 bitri k × r v x r k × x v
125 ssin k × r v k × r k × X k × r v k × X
126 117 124 125 3bitr3g R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R x r k × x v k × r v k × X
127 99 adantr R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R k = S 𝑡 k
128 127 xpeq1d R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R k × r = S 𝑡 k × r
129 128 sseq1d R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R k × r v k × X S 𝑡 k × r v k × X
130 114 126 129 3bitrd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R r x X | k × x v S 𝑡 k × r v k × X
131 130 anbi2d R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R w r r x X | k × x v w r S 𝑡 k × r v k × X
132 131 rexbidva R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R w r r x X | k × x v r R w r S 𝑡 k × r v k × X
133 109 132 mpbird R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w X k × w v r R w r r x X | k × x v
134 58 133 sylan2b R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w x X | k × x v r R w r r x X | k × x v
135 134 ralrimiva R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp w x X | k × x v r R w r r x X | k × x v
136 eltop2 R Top x X | k × x v R w x X | k × x v r R w r r x X | k × x v
137 14 68 136 3syl R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X | k × x v R w x X | k × x v r R w r r x X | k × x v
138 135 137 mpbird R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X | k × x v R
139 54 138 eqeltrd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp x X | y Y y x f S Cn S × t R | f k v R
140 imaeq2 z = f S Cn S × t R | f k v F -1 z = F -1 f S Cn S × t R | f k v
141 1 mptpreima F -1 f S Cn S × t R | f k v = x X | y Y y x f S Cn S × t R | f k v
142 140 141 eqtrdi z = f S Cn S × t R | f k v F -1 z = x X | y Y y x f S Cn S × t R | f k v
143 142 eleq1d z = f S Cn S × t R | f k v F -1 z R x X | y Y y x f S Cn S × t R | f k v R
144 139 143 syl5ibrcom R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp z = f S Cn S × t R | f k v F -1 z R
145 144 expimpd R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp z = f S Cn S × t R | f k v F -1 z R
146 145 rexlimdvva R TopOn X S TopOn Y k 𝒫 S v S × t R S 𝑡 k Comp z = f S Cn S × t R | f k v F -1 z R
147 13 146 syl5bi R TopOn X S TopOn Y z ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v F -1 z R
148 147 ralrimiv R TopOn X S TopOn Y z ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v F -1 z R
149 simpl R TopOn X S TopOn Y R TopOn X
150 ovex S Cn S × t R V
151 150 pwex 𝒫 S Cn S × t R V
152 9 10 11 xkotf k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v : w 𝒫 S | S 𝑡 w Comp × S × t R 𝒫 S Cn S × t R
153 frn k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v : w 𝒫 S | S 𝑡 w Comp × S × t R 𝒫 S Cn S × t R ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v 𝒫 S Cn S × t R
154 152 153 ax-mp ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v 𝒫 S Cn S × t R
155 151 154 ssexi ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v V
156 155 a1i R TopOn X S TopOn Y ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v V
157 9 10 11 xkoval S Top S × t R Top S × t R ^ ko S = topGen fi ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v
158 67 70 157 syl2anc R TopOn X S TopOn Y S × t R ^ ko S = topGen fi ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v
159 eqid S × t R ^ ko S = S × t R ^ ko S
160 159 xkotopon S Top S × t R Top S × t R ^ ko S TopOn S Cn S × t R
161 67 70 160 syl2anc R TopOn X S TopOn Y S × t R ^ ko S TopOn S Cn S × t R
162 149 156 158 161 subbascn R TopOn X S TopOn Y F R Cn S × t R ^ ko S F : X S Cn S × t R z ran k w 𝒫 S | S 𝑡 w Comp , v S × t R f S Cn S × t R | f k v F -1 z R
163 8 148 162 mpbir2and R TopOn X S TopOn Y F R Cn S × t R ^ ko S