Theorem xpcn 7926

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

Step	Hyp	Ref	Expression
1		ffvelrn 3805	. . . . . . . . 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)
8	4, 5, 6, 7	metcnf 7836	. . . . . . . . . 10 |- ((A e. Met /\ B e. Met /\ F e. (J Cn K)) -> F:X-->Y)
9	2, 3, 8	mp3an12 904	. . . . . . . . 9 |- (F e. (J Cn K) -> F:X-->Y)
10	1, 9	sylan 448	. . . . . . . 8 |- ((F e. (J Cn K) /\ w e. X) -> (F` w) e. Y)
11		ffvelrn 3805	. . . . . . . . 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)
15	4, 13, 6, 14	metcnf 7836	. . . . . . . . . 10 |- ((A e. Met /\ C e. Met /\ G e. (J Cn L)) -> G:X-->Z)
16	2, 12, 15	mp3an12 904	. . . . . . . . 9 |- (G e. (J Cn L) -> G:X-->Z)
17	11, 16	sylan 448	. . . . . . . 8 |- ((G e. (J Cn L) /\ w e. X) -> (G` w) e. Z)
18	10, 17	anim12i 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))
19	18	anandirs 513	. . . . . 6 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ w e. X) -> ((F` w) e. Y /\ (G` w) e. Z))
20		opelxpi 3212	. . . . . 6 |- (((F` w) e. Y /\ (G` w) e. Z) -> <.(F` w), (G` w)>. e. (Y X. Z))
21	19, 20	syl 10	. . . . 5 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ w e. X) -> <.(F` w), (G` w)>. e. (Y X. Z))
22	21	r19.21aiva 1711	. . . 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)>.)}
24	23	fopab2 3814	. . . 4 |- (A.w e. X <.(F` w), (G` w)>. e. (Y X. Z) <-> H:X-->(Y X. Z))
25	22, 24	sylib 198	. . 3 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> H:X-->(Y X. Z))
26	4, 6, 5, 7	metcni 7846	. . . . . . . . . 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)))
27	2, 26	mp3anl1 908	. . . . . . . . 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)))
28	3, 27	mpanl1 705	. . . . . . . 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)))
29	28	adantlr 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)))
30	4, 6, 13, 14	metcni 7846	. . . . . . . . . 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)))
31	2, 30	mp3anl1 908	. . . . . . . . 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)))
32	12, 31	mpanl1 705	. . . . . . . 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)))
33	32	adantll 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 2618	. . . . . . . . . . . . . . 15 |- (s = if(p <_ q, p, q) -> (0 < s <-> 0 < if(p <_ q, p, q)))
35		breq2 2618	. . . . . . . . . . . . . . . . 17 |- (s = if(p <_ q, p, q) -> ((uAr) < s <-> (uAr) < if(p <_ q, p, q)))
36	35	imbi1d 612	. . . . . . . . . . . . . . . 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)))
37	36	ralbidv 1660	. . . . . . . . . . . . . . 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)))
38	34, 37	anbi12d 627	. . . . . . . . . . . . . 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))))
39	38	rcla4ev 1873	. . . . . . . . . . . . 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 2376	. . . . . . . . . . . . . 14 |- ((p e. RR /\ q e. RR) -> if(p <_ q, p, q) e. RR)
41	40	ad2antlr 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 2618	. . . . . . . . . . . . . . . 16 |- (p = if(p <_ q, p, q) -> (0 < p <-> 0 < if(p <_ q, p, q)))
43		breq2 2618	. . . . . . . . . . . . . . . 16 |- (q = if(p <_ q, p, q) -> (0 < q <-> 0 < if(p <_ q, p, q)))
44	42, 43	ifboth 2371	. . . . . . . . . . . . . . 15 |- ((0 < p /\ 0 < q) -> 0 < if(p <_ q, p, q))
45	44	ad2antrl 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) /\