Theorem xpcn 8187

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 3928	. . . . . . . . 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 8095	. . . . . . . . . 10 |- ((A e. Met /\ B e. Met /\ F e. (J Cn K)) -> F:X-->Y)
9	2, 3, 8	mp3an12 912	. . . . . . . . 9 |- (F e. (J Cn K) -> F:X-->Y)
10	1, 9	sylan 450	. . . . . . . 8 |- ((F e. (J Cn K) /\ w e. X) -> (F` w) e. Y)
11		ffvelrn 3928	. . . . . . . . 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 8095	. . . . . . . . . 10 |- ((A e. Met /\ C e. Met /\ G e. (J Cn L)) -> G:X-->Z)
16	2, 12, 15	mp3an12 912	. . . . . . . . 9 |- (G e. (J Cn L) -> G:X-->Z)
17	11, 16	sylan 450	. . . . . . . 8 |- ((G e. (J Cn L) /\ w e. X) -> (G` w) e. Z)
18	10, 17	anim12i 331	. . . . . . 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 516	. . . . . 6 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ w e. X) -> ((F` w) e. Y /\ (G` w) e. Z))
20		opelxpi 3300	. . . . . 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 1760	. . . 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 3937	. . . 4 |- (A.w e. X <.(F` w), (G` w)>. e. (Y X. Z) <-> H:X-->(Y X. Z))
25	22, 24	sylib 196	. . 3 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> H:X-->(Y X. Z))
26	4, 6, 5, 7	metcni 8105	. . . . . . . . . 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 916	. . . . . . . . 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 710	. . . . . . . 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 8105	. . . . . . . . . 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 916	. . . . . . . . 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 710	. . . . . . . 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 2696	. . . . . . . . . . . . . . 15 |- (s = if(p <_ q, p, q) -> (0 < s <-> 0 < if(p <_ q, p, q)))
35		breq2 2696	. . . . . . . . . . . . . . . . 17 |- (s = if(p <_ q, p, q) -> ((uAr) < s <-> (uAr) < if(p <_ q, p, q)))
36	35	imbi1d 616	. . . . . . . . . . . . . . . 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 1709	. . . . . . . . . . . . . . 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 631	. . . . . . . . . . . . . 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 1923	. . . . . . . . . . . . 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 2434	. . . . . . . . . . . . . 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 2696	. . . . . . . . . . . . . . . 16 |- (p = if(p <_ q, p, q) -> (0 < p <-> 0 < if(p <_ q, p, q)))
43		breq2 2696	. . . . . . . . . . . . . . . 16 |- (q = if(p <_ q, p, q) -> (0 < q <-> 0 < if(p <_ q, p, q)))
44	42, 43	ifboth 2429	. . . . . . . . . . . . . . 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) /\ A.r e. X (((uAr) < p -> ((F` u)B(F` r)) < t) /\ ((uAr) < q -> ((G` u)C(G` r)) < t)))) -> 0 < if(p <_ q, p, q))
46		ltmin 6068	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((uAr) e. RR /\ p e. RR /\ q e. RR) -> ((uAr) < if(p <_ q, p, q) <-> ((uAr) < p /\ (uAr) < q)))
47	46	biimpd 151	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((uAr) e. RR /\ p e. RR /\ q e. RR) -> ((uAr) < if(p <_ q, p, q) -> ((uAr) < p /\ (uAr) < q)))
48	4	metcl 8021	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A e. Met /\ u e. X /\ r e. X) -> (uAr) e. RR)
49	2, 48	mp3an1 909	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((u e. X /\ r e. X) -> (uAr) e. RR)
50	49	3ad2antl1 815	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((u e. X /\ t e. RR /\ 0 < t) /\ r e. X) -> (uAr) e. RR)
51	47, 50	syl3an1 865	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. X /\ t e. RR /\ 0 < t) /\ r e. X) /\ p e. RR /\ q e. RR) -> ((uAr) < if(p <_ q, p, q) -> ((uAr) < p /\ (uAr) < q)))
52	51	3expb 840	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((u e. X /\ t e. RR /\ 0 < t) /\ r e. X) /\ (p e. RR /\ q e. RR)) -> ((uAr) < if(p <_ q, p, q) -> ((uAr) < p /\ (uAr) < q)))
53	52	an1rs 492	. . . . . . . . . . . . . . . . . . . . 21 |- ((((u e. X /\ t e. RR /\ 0 < t) /\ (p e. RR /\ q e. RR)) /\ r e. X) -> ((uAr) < if(p <_ q, p, q) -> ((uAr) < p /\ (uAr) < q)))
54	53	adantlll 396	. . . . . . . . . . . . . . . . . . . 20 |- (((((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) /\ (p e. RR /\ q e. RR)) /\ r e. X) -> ((uAr) < if(p <_ q, p, q) -> ((uAr) < p /\ (uAr) < q)))
55		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = u -> (F` w) = (F` u))
56		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = u -> (G` w) = (G` u))
57	55, 56	opeq12d 2560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = u -> <.(F` w), (G` w)>. = <.(F` u), (G` u)>.)
58		opex 2858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- <.(F` u), (G` u)>. e. V
59	57, 23, 58	fvopab4 3891	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (u e. X -> (H` u) = <.(F` u), (G` u)>.)
60		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = r -> (F` w) = (F` r))
61		fveq2 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w = r -> (G` w) = (G` r))
62	60, 61	opeq12d 2560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = r -> <.(F` w), (G` w)>. = <.(F` r), (G` r)>.)
63		opex 2858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- <.(F` r), (G` r)>. e. V
64	62, 23, 63	fvopab4 3891	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (r e. X -> (H` r) = <.(F` r), (G` r)>.)
65	59, 64	opreqan12d 4037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. X /\ r e. X) -> ((H` u)D(H` r)) = (<.(F` u), (G` u)>.D<.(F` r), (G` r)>.))
66	65	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ r e. X)) -> ((H` u)D(H` r)) = (<.(F` u), (G` u)>.D<.(F` r), (G` r)>.))
67		xpcn.10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- 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, < ))}
68		fvex 3843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (F` u) e. V
69	68	op1st 4146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (1st` <.(F` u), (G` u)>.) = (F` u)
70	69	eqcomi 1522	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (F` u) = (1st` <.(F` u), (G` u)>.)
71		fvex 3843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (G` u) e. V
72	68, 71	op2nd 4147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (2nd` <.(F` u), (G` u)>.) = (G` u)
73	72	eqcomi 1522	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (G` u) = (2nd` <.(F` u), (G` u)>.)
74		fvex 3843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (F` r) e. V
75	74	op1st 4146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (1st` <.(F` r), (G` r)>.) = (F` r)
76	75	eqcomi 1522	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (F` r) = (1st` <.(F` r), (G` r)>.)
77		fvex 3843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (G` r) e. V
78	74, 77	op2nd 4147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (2nd` <.(F` r), (G` r)>.) = (G` r)
79	78	eqcomi 1522	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (G` r) = (2nd` <.(F` r), (G` r)>.)
80	5, 13, 3, 12, 67, 70, 73, 76, 79	metxpdval 8039	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((<.(F` u), (G` u)>. e. (Y X. Z) /\ <.(F` r), (G` r)>. e. (Y X. Z)) -> (<.(F` u), (G` u)>.D<.(F` r), (G` r)>.) = if(((G` u)C(G` r)) < ((F` u)B(F` r)), ((F` u)B(F` r)), ((G` u)C(G` r))))
81		opelxpi 3300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F` u) e. Y /\ (G` u) e. Z) -> <.(F` u), (G` u)>. e. (Y X. Z))
82		ffvelrn 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((F:X-->Y /\ u e. X) -> (F` u) e. Y)
83	82, 9	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F e. (J Cn K) /\ u e. X) -> (F` u) e. Y)
84		ffvelrn 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((G:X-->Z /\ u e. X) -> (G` u) e. Z)
85	84, 16	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((G e. (J Cn L) /\ u e. X) -> (G` u) e. Z)
86	81, 83, 85	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F e. (J Cn K) /\ u e. X) /\ (G e. (J Cn L) /\ u e. X)) -> <.(F` u), (G` u)>. e. (Y X. Z))
87	86	anandirs 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ u e. X) -> <.(F` u), (G` u)>. e. (Y X. Z))
88	87	adantrr 395	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ r e. X)) -> <.(F` u), (G` u)>. e. (Y X. Z))
89		opelxpi 3300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F` r) e. Y /\ (G` r) e. Z) -> <.(F` r), (G` r)>. e. (Y X. Z))
90		ffvelrn 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((F:X-->Y /\ r e. X) -> (F` r) e. Y)
91	90, 9	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((F e. (J Cn K) /\ r e. X) -> (F` r) e. Y)
92		ffvelrn 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((G:X-->Z /\ r e. X) -> (G` r) e. Z)
93	92, 16	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((G e. (J Cn L) /\ r e. X) -> (G` r) e. Z)
94	89, 91, 93	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F e. (J Cn K) /\ r e. X) /\ (G e. (J Cn L) /\ r e. X)) -> <.(F` r), (G` r)>. e. (Y X. Z))
95	94	anandirs 516	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ r e. X) -> <.(F` r), (G` r)>. e. (Y X. Z))
96	95	adantrl 394	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ r e. X)) -> <.(F` r), (G` r)>. e. (Y X. Z))
97	80, 88, 96	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ r e. X)) -> (<.(F` u), (G` u)>.D<.(F` r), (G` r)>.) = if(((G` u)C(G` r)) < ((F` u)B(F` r)), ((F` u)B(F` r)), ((G` u)C(G` r))))
98	66, 97	eqtrd 1550	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ r e. X)) -> ((H` u)D(H` r)) = if(((G` u)C(G` r)) < ((F` u)B(F` r)), ((F` u)B(F` r)), ((G` u)C(G` r))))
99	98	breq1d 2702	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ r e. X)) -> (((H` u)D(H` r)) < t <-> if(((G` u)C(G` r)) < ((F` u)B(F` r)), ((F` u)B(F` r)), ((G` u)C(G` r))) < t))
100		breq1 2695	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` u)B(F` r)) = if(((G` u)C(G` r)) < ((F` u)B(F` r)), ((F` u)B(F` r)), ((G` u)C(G` r))) -> (((F` u)B(F` r)) < t <-> if(((G` u)C(G` r)) < ((F` u)B(F` r)), ((F` u)B(F` r)), ((G` u)C(G` r))) < t))
101		breq1 2695	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((G` u)C(G` r)) = if(((G` u)C(G` r)) < ((F` u)B(F` r)), ((F` u)B(F` r)), ((G` u)C(G` r))) -> (((G` u)C(G` r)) < t <-> if(((G` u)C(G` r)) < ((F` u)B(F` r)), ((F` u)B(F` r)), ((G` u)C(G` r))) < t))
102	100, 101	ifboth 2429	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((F` u)B(F` r)) < t /\ ((G` u)C(G` r)) < t) -> if(((G` u)C(G` r)) < ((F` u)B(F` r)), ((F` u)B(F` r)), ((G` u)C(G` r))) < t)
103	99, 102	syl5bir 208	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ r e. X)) -> ((((F` u)B(F` r)) < t /\ ((G` u)C(G` r)) < t) -> ((H` u)D(H` r)) < t))
104	103	anassrs 443	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((F e. (J Cn K) /\ G e. (J Cn L)) /\ u e. X) /\ r e. X) -> ((((F` u)B(F` r)) < t /\ ((G` u)C(G` r)) < t) -> ((H` u)D(H` r)) < t))
105		3simp1 794	. . . . . . . . . . . . . . . . . . . . . 22 |- ((u e. X /\ t e. RR /\ 0 < t) -> u e. X)
106	104, 105	sylanl2 463	. . . . . . . . . . . . . . . . . . . . 21 |- ((((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) /\ r e. X) -> ((((F` u)B(F` r)) < t /\ ((G` u)C(G` r)) < t) -> ((H` u)D(H` r)) < t))
107	106	adantlr 393	. . . . . . . . . . . . . . . . . . . 20 |- (((((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) /\ (p e. RR /\ q e. RR)) /\ r e. X) -> ((((F` u)B(F` r)) < t /\ ((G` u)C(G` r)) < t) -> ((H` u)D(H` r)) < t))
108	54, 107	imim12d 29	. . . . . . . . . . . . . . . . . . 19 |- (((((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) /\ (p e. RR /\ q e. RR)) /\ r e. X) -> ((((uAr) < p /\ (uAr) < q) -> (((F` u)B(F` r)) < t /\ ((G` u)C(G` r)) < t)) -> ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t)))
109	108	adantlr 393	. . . . . . . . . . . . . . . . . 18 |- ((((((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)) /\ r e. X) -> ((((uAr) < p /\ (uAr) < q) -> (((F` u)B(F` r)) < t /\ ((G` u)C(G` r)) < t)) -> ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t)))
110		prth 559	. . . . . . . . . . . . . . . . . 18 |- ((((uAr) < p -> ((F` u)B(F` r)) < t) /\ ((uAr) < q -> ((G` u)C(G` r)) < t)) -> (((uAr) < p /\ (uAr) < q) -> (((F` u)B(F` r)) < t /\ ((G` u)C(G` r)) < t)))
111	109, 110	syl5 21	. . . . . . . . . . . . . . . . 17 |- ((((((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)) /\ r e. X) -> ((((uAr) < p -> ((F` u)B(F` r)) < t) /\ ((uAr) < q -> ((G` u)C(G` r)) < t)) -> ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t)))
112	111	r19.20dva 1755	. . . . . . . . . . . . . . . 16 |- (((((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)) -> A.r e. X ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t)))
113	112	imp 348	. . . . . . . . . . . . . . 15 |- ((((((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))) -> A.r e. X ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t))
114	113	anasss 442	. . . . . . . . . . . . . 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) /\ A.r e. X (((uAr) < p -> ((F` u)B(F` r)) < t) /\ ((uAr) < q -> ((G` u)C(G` r)) < t)))) -> A.r e. X ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t))
115	45, 114	jca 286	. . . . . . . . . . . . 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)))) -> (0 < if(p <_ q, p, q) /\ A.r e. X ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t)))
116	39, 41, 115	sylanc 473	. . . . . . . . . . . 12 |- (((((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)))) -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t)))
117	116	ex 371	. . . . . . . . . . 11 |- ((((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))) -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t))))
118		an4 509	. . . . . . . . . . . 12 |- (((0 < p /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)) /\ (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))) <-> ((0 < p /\ 0 < q) /\ (A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t) /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))))
119		r19.26 1796	. . . . . . . . . . . . 13 |- (A.r e. X (((uAr) < p -> ((F` u)B(F` r)) < t) /\ ((uAr) < q -> ((G` u)C(G` r)) < t)) <-> (A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t) /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t)))
120	119	anbi2i 483	. . . . . . . . . . . 12 |- (((0 < p /\ 0 < q) /\ A.r e. X (((uAr) < p -> ((F` u)B(F` r)) < t) /\ ((uAr) < q -> ((G` u)C(G` r)) < t))) <-> ((0 < p /\ 0 < q) /\ (A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t) /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))))
121	118, 120	bitr4i 174	. . . . . . . . . . 11 |- (((0 < p /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)) /\ (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))) <-> ((0 < p /\ 0 < q) /\ A.r e. X (((uAr) < p -> ((F` u)B(F` r)) < t) /\ ((uAr) < q -> ((G` u)C(G` r)) < t))))
122	117, 121	syl5ib 204	. . . . . . . . . 10 |- ((((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 /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)) /\ (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))) -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t))))
123	122	ex 371	. . . . . . . . 9 |- (((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 /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)) /\ (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))) -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t)))))
124	123	r19.23advv 1795	. . . . . . . 8 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) -> (E.p e. RR E.q e. RR ((0 < p /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)) /\ (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))) -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t))))
125		reeanv 1824	. . . . . . . 8 |- (E.p e. RR E.q e. RR ((0 < p /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)) /\ (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))) <-> (E.p e. RR (0 < p /\ A.r e. X ((uAr) < p -> ((F` u)B(F` r)) < t)) /\ E.q e. RR (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))))
126	124, 125	syl5ibr 205	. . . . . . 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)) /\ E.q e. RR (0 < q /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))) -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t))))
127	29, 33, 126	mp2and 707	. . . . . 6 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ t e. RR /\ 0 < t)) -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t)))
128	127	3exp2 857	. . . . 5 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> (u e. X -> (t e. RR -> (0 < t -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t))))))
129	128	imp3a 359	. . . 4 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> ((u e. X /\ t e. RR) -> (0 < t -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t)))))
130	129	r19.21aivv 1766	. . 3 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> A.u e. X A.t e. RR (0 < t -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t))))
131	25, 130	jca 286	. 2 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> (H:X-->(Y X. Z) /\ A.u e. X A.t e. RR (0 < t -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t)))))
132	5, 13, 3, 12, 67	metxp 8044	. . 3 |- D e. Met
133		ltso 5666	. . . . . . . 8 |- < Or RR
134	133	supex 4720	. . . . . . 7 |- sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ) e. V
135	134, 67	dmoprab2 4185	. . . . . 6 |- dom D = ((Y X. Z) X. (Y X. Z))
136	135	dmeqi 3403	. . . . 5 |- dom dom D = dom ((Y X. Z) X. (Y X. Z))
137		dmxpid 3420	. . . . 5 |- dom ((Y X. Z) X. (Y X. Z)) = (Y X. Z)
138	136, 137	eqtr2i 1539	. . . 4 |- (Y X. Z) = dom dom D
139		xpcn.11b	. . . 4 |- M = (Open` D)
140	4, 6, 138, 139	metcn 8100	. . 3 |- ((A e. Met /\ D e. Met) -> (H e. (J Cn M) <-> (H:X-->(Y X. Z) /\ A.u e. X A.t e. RR (0 < t -> E.s e. RR (0 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t))))))
141	2, 132, 140	mp2an 701	. 2 |- (H e. (J Cn M) <-> (H:X-->(Y X. Z) /\ A.u e. X A.t e. RR (0 < t -> E.s e. RR (0