HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem xpcn 7910
Description: Construct a continuous function to the product of the codomains of two continuous functions on a common metric space. Warning: The HTML proof page is 0.5MB in size.
Hypotheses
Ref Expression
xpcn.1 |- X = dom dom A
xpcn.3 |- Y = dom dom B
xpcn.5 |- Z = dom dom C
xpcn.7 |- A e. Met
xpcn.8 |- B e. Met
xpcn.9 |- C e. Met
xpcn.10 |- D = {<.<.x, y>., z>. | ((x e. (Y X. Z) /\ y e. (Y X. Z)) /\ z = sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}
xpcn.11 |- J = (Open` A)
xpcn.12 |- K = (Open` B)
xpcn.11a |- L = (Open` C)
xpcn.11b |- M = (Open` D)
xpcn.13 |- H = {<.w, v>. | (w e. X /\ v = <.(F` w), (G` w)>.)}
Assertion
Ref Expression
xpcn |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> H e. (J Cn M))
Distinct variable groups:   x,y,z,B   x,C,y,z   w,v,x,y,z,F   v,G,w,x,y,z   w,J   w,K   w,L   v,X,w   v,Y,w,x,y,z   v,Z,w,x,y,z
Proof of Theorem xpcn
StepHypRef Expression
1 ffvelrn 3799 . . . . . . . . 9 |- ((F:X-->Y /\ w e. X) -> (F` w) e. Y)
2 xpcn.7 . . . . . . . . . 10 |- A e. Met
3 xpcn.8 . . . . . . . . . 10 |- B e. Met
4 xpcn.1 . . . . . . . . . . 11 |- X = dom dom A
5 xpcn.3 . . . . . . . . . . 11 |- Y = dom dom B
6 xpcn.11 . . . . . . . . . . 11 |- J = (Open` A)
7 xpcn.12 . . . . . . . . . . 11 |- K = (Open` B)
84, 5, 6, 7metcnf 7823 . . . . . . . . . 10 |- ((A e. Met /\ B e. Met /\ F e. (J Cn K)) -> F:X-->Y)
92, 3, 8mp3an12 903 . . . . . . . . 9 |- (F e. (J Cn K) -> F:X-->Y)
101, 9sylan 448 . . . . . . . 8 |- ((F e. (J Cn K) /\ w e. X) -> (F` w) e. Y)
11 ffvelrn 3799 . . . . . . . . 9 |- ((G:X-->Z /\ w e. X) -> (G` w) e. Z)
12 xpcn.9 . . . . . . . . . 10 |- C e. Met
13 xpcn.5 . . . . . . . . . . 11 |- Z = dom dom C
14 xpcn.11a . . . . . . . . . . 11 |- L = (Open` C)
154, 13, 6, 14metcnf 7823 . . . . . . . . . 10 |- ((A e. Met /\ C e. Met /\ G e. (J Cn L)) -> G:X-->Z)
162, 12, 15mp3an12 903 . . . . . . . . 9 |- (G e. (J Cn L) -> G:X-->Z)
1711, 16sylan 448 . . . . . . . 8 |- ((G e. (J Cn L) /\ w e. X) -> (G` w) e. Z)
1810, 17anim12i 333 . . . . . . 7 |- (((F e. (J Cn K) /\ w e. X) /\ (G e. (J Cn L) /\ w e. X)) -> ((F` w) e. Y /\ (G` w) e. Z))
1918anandirs 512 . . . . . 6 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ w e. X) -> ((F` w) e. Y /\ (G` w) e. Z))
20 opelxpi 3207 . . . . . 6 |- (((F` w) e. Y /\ (G` w) e. Z) -> <.(F` w), (G` w)>. e. (Y X. Z))
2119, 20syl 10 . . . . 5 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ w e. X) -> <.(F` w), (G` w)>. e. (Y X. Z))
2221r19.21aiva 1706 . . . 4 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> A.w e. X <.(F` w), (G` w)>. e. (Y X. Z))
23 xpcn.13 . . . . 5 |- H = {<.w, v>. | (w e. X /\ v = <.(F` w), (G` w)>.)}
2423fopab2 3808 . . . 4 |- (A.w e. X <.(F` w), (G` w)>. e. (Y X. Z) <-> H:X-->(Y X. Z))
2522, 24sylib 198 . . 3 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> H:X-->(Y X. Z))
264, 6, 5, 7metcni 7833 . . . . . . . . . 10 |- (((A e. Met /\ B e. Met /\ F e. (J Cn K)) /\ (u e. X /\ t e. RR /\ 0 < t)) -> E.p e. RR (0 < p /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)))
272, 26mp3anl1 907 . . . . . . . . 9 |- (((B e. Met /\ F e. (J Cn K)) /\ (u e. X /\ t e. RR /\ 0 < t)) -> E.p e. RR (0 < p /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)))
283, 27mpanl1 704 . . . . . . . 8 |- ((F e. (J Cn K) /\ (u e. X /\ t e. RR /\ 0 < t)) -> E.p e. RR (0 < p /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)))
2928adantlr 393 . . . . . . 7 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) -> E.p e. RR (0 < p /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)))
304, 6, 13, 14metcni 7833 . . . . . . . . . 10 |- (((A e. Met /\ C e. Met /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) -> E.q e. RR (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t)))
312, 30mp3anl1 907 . . . . . . . . 9 |- (((C e. Met /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) -> E.q e. RR (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t)))
3212, 31mpanl1 704 . . . . . . . 8 |- ((G e. (J Cn L) /\ (u e. X /\ t e. RR /\ 0 < t)) -> E.q e. RR (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t)))
3332adantll 392 . . . . . . 7 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) -> E.q e. RR (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t)))
34 breq2 2613 . . . . . . . . . . . . . . 15 |- (s = if(p <_ q, p, q) -> (0 < s <-> 0 < if(p <_ q, p, q)))
35 breq2 2613 . . . . . . . . . . . . . . . . 17 |- (s = if(p <_ q, p, q) -> ((uAr) < s <-> (uAr) < if(p <_ q, p, q)))
3635imbi1d 611 . . . . . . . . . . . . . . . 16 |- (s = if(p <_ q, p, q) -> (((uAr) < s -> ((H` u)D(H` r)) < t) <-> ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t)))
3736ralbidv 1655 . . . . . . . . . . . . . . 15 |- (s = if(p <_ q, p, q) -> (A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t) <-> A.r e. X ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t)))
3834, 37anbi12d 626 . . . . . . . . . . . . . 14 |- (s = if(p <_ q, p, q) -> ((0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t)) <-> (0 < if(p <_ q, p, q) /\ A.r e. X ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t))))
3938rcla4ev 1868 . . . . . . . . . . . . 13 |- ((if(p <_ q, p, q) e. RR /\ (0 < if(p <_ q, p, q) /\ A.r e. X ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t))) -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t)))
40 ifcl 2370 . . . . . . . . . . . . . 14 |- ((p e. RR /\ q e. RR) -> if(p <_ q, p, q) e. RR)
4140ad2antlr 405 . . . . . . . . . . . . 13 |- (((((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) /\ (p e. RR /\ q e. RR)) /\ ((0 < p /\ 0 < q) /\ A.r e. X (((uAr) < p -> ((F` u)B(F` r)) < t) /\ ((uAr) < q -> ((G` u)C(G` r)) < t)))) -> if(p <_ q, p, q) e. RR)
42 breq2 2613 . . . . . . . . . . . . . . . 16 |- (p = if(p <_ q, p, q) -> (0 < p <-> 0 < if(p <_ q, p, q)))
43 breq2 2613 . . . . . . . . . . . . . . . 16 |- (q = if(p <_ q, p, q) -> (0 < q <-> 0 < if(p <_ q, p, q)))
4442, 43ifboth 2365 . . . . . . . . . . . . . . 15 |- ((0 < p /\ 0 < q) -> 0 < if(p <_ q, p, q))
4544ad2antrl 406 . . . . . . . . . . . . . 14 |- (((((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) /\ (p e. RR /\ q e. RR)) /\ ((0 < p /\ 0 < q) /\