Theorem xpcn 9254

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		xpcn.7	. . 3 |- A e. Met
2		xpcn.3	. . . 4 |- Y = dom dom B
3		xpcn.5	. . . 4 |- Z = dom dom C
4		xpcn.8	. . . 4 |- B e. Met
5		xpcn.9	. . . 4 |- C e. Met
6		xpcn.10	. . . 4 |- 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, < ))}
7	2, 3, 4, 5, 6	metxp 9111	. . 3 |- D e. Met
8		xpcn.1	. . . 4 |- X = dom dom A
9		xpcn.11	. . . 4 |- J = (Open` A)
10		ltso 6681	. . . . . . . 8 |- < Or RR
11	10	supex 5667	. . . . . . 7 |- sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ) e. _V
12	11, 6	dmoprab2 5065	. . . . . 6 |- dom D = ((Y X. Z) X. (Y X. Z))
13	12	dmeqi 4158	. . . . 5 |- dom dom D = dom ((Y X. Z) X. (Y X. Z))
14		dmxpid 4179	. . . . 5 |- dom ((Y X. Z) X. (Y X. Z)) = (Y X. Z)
15	13, 14	eqtr2i 1909	. . . 4 |- (Y X. Z) = dom dom D
16		xpcn.11b	. . . 4 |- M = (Open` D)
17	8, 9, 15, 16	metcn 9167	. . 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))))))
18	1, 7, 17	mp2an 761	. 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 < s /\ A.r e. X ((uAr) < s -> ((H` u)D(H` r)) < t)))))
19		ffvelrn 4787	. . . . . . . 8 |- ((F:X-->Y /\ w e. X) -> (F` w) e. Y)
20		xpcn.12	. . . . . . . . . 10 |- K = (Open` B)
21	8, 2, 9, 20	metcnf 9162	. . . . . . . . 9 |- ((A e. Met /\ B e. Met /\ F e. (J Cn K)) -> F:X-->Y)
22	1, 4, 21	mp3an12 1181	. . . . . . . 8 |- (F e. (J Cn K) -> F:X-->Y)
23	19, 22	sylan 497	. . . . . . 7 |- ((F e. (J Cn K) /\ w e. X) -> (F` w) e. Y)
24		ffvelrn 4787	. . . . . . . 8 |- ((G:X-->Z /\ w e. X) -> (G` w) e. Z)
25		xpcn.11a	. . . . . . . . . 10 |- L = (Open` C)
26	8, 3, 9, 25	metcnf 9162	. . . . . . . . 9 |- ((A e. Met /\ C e. Met /\ G e. (J Cn L)) -> G:X-->Z)
27	1, 5, 26	mp3an12 1181	. . . . . . . 8 |- (G e. (J Cn L) -> G:X-->Z)
28	24, 27	sylan 497	. . . . . . 7 |- ((G e. (J Cn L) /\ w e. X) -> (G` w) e. Z)
29	23, 28	anim12i 360	. . . . . 6 |- (((F e. (J Cn K) /\ w e. X) /\ (G e. (J Cn L) /\ w e. X)) -> ((F` w) e. Y /\ (G` w) e. Z))
30	29	anandirs 571	. . . . 5 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ w e. X) -> ((F` w) e. Y /\ (G` w) e. Z))
31		opelxpi 4040	. . . . 5 |- (((F` w) e. Y /\ (G` w) e. Z) -> <.(F` w), (G` w)>. e. (Y X. Z))
32	30, 31	syl 12	. . . 4 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ w e. X) -> <.(F` w), (G` w)>. e. (Y X. Z))
33	32	r19.21aiva 2176	. . 3 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> A.w e. X <.(F` w), (G` w)>. e. (Y X. Z))
34		xpcn.13	. . . 4 |- H = {<.w, v>. | (w e. X /\ v = <.(F` w), (G` w)>.)}
35	34	fopab2 4796	. . 3 |- (A.w e. X <.(F` w), (G` w)>. e. (Y X. Z) <-> H:X-->(Y X. Z))
36	33, 35	sylib 215	. 2 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> H:X-->(Y X. Z))
37	8, 9, 2, 20	metcni 9172	. . . . . . . . 9 |- (((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)))
38	1, 37	mp3anl1 1185	. . . . . . . 8 |- (((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)))
39	4, 38	mpanl1 770	. . . . . . 7 |- ((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)))
40	39	adantlr 429	. . . . . 6 |- (((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)))
41	8, 9, 3, 25	metcni 9172	. . . . . . . . 9 |- (((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)))
42	1, 41	mp3anl1 1185	. . . . . . . 8 |- (((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)))
43	5, 42	mpanl1 770	. . . . . . 7 |- ((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)))
44	43	adantll 428	. . . . . 6 |- (((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)))
45		ifcl 3007	. . . . . . . . . . . . 13 |- ((p e. RR /\ q e. RR) -> if(p <_ q, p, q) e. RR)
46	45	ad2antlr 441	. . . . . . . . . . . 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)))) -> if(p <_ q, p, q) e. RR)
47		breq2 3342	. . . . . . . . . . . . . 14 |- (p = if(p <_ q, p, q) -> (0 < p <-> 0 < if(p <_ q, p, q)))
48		breq2 3342	. . . . . . . . . . . . . 14 |- (q = if(p <_ q, p, q) -> (0 < q <-> 0 < if(p <_ q, p, q)))
49	47, 48	ifboth 3002	. . . . . . . . . . . . 13 |- ((0 < p /\ 0 < q) -> 0 < if(p <_ q, p, q))
50	49	ad2antrl 442	. . . . . . . . . . . 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)))) -> 0 < if(p <_ q, p, q))
51		ltmin 7106	. . . . . . . . . . . . . . . . . . . . . 22 |- (((uAr) e. RR /\ p e. RR /\ q e. RR) -> ((uAr) < if(p <_ q, p, q) <-> ((uAr) < p /\ (uAr) < q)))
52	51	biimpd 170	. . . . . . . . . . . . . . . . . . . . 21 |- (((uAr) e. RR /\ p e. RR /\ q e. RR) -> ((uAr) < if(p <_ q, p, q) -> ((uAr) < p /\ (uAr) < q)))
53	8	metcl 9088	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((A e. Met /\ u e. X /\ r e. X) -> (uAr) e. RR)
54	1, 53	mp3an1 1178	. . . . . . . . . . . . . . . . . . . . . 22 |- ((u e. X /\ r e. X) -> (uAr) e. RR)
55	54	3ad2antl1 1038	. . . . . . . . . . . . . . . . . . . . 21 |- (((u e. X /\ t e. RR /\ 0 < t) /\ r e. X) -> (uAr) e. RR)
56	52, 55	syl3an1 1130	. . . . . . . . . . . . . . . . . . . 20 |- ((((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)))
57	56	3expb 1068	. . . . . . . . . . . . . . . . . . 19 |- ((((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)))
58	57	an1rs 547	. . . . . . . . . . . . . . . . . 18 |- ((((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)))
59	58	adantlll 432	. . . . . . . . . . . . . . . . 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)) /\ r e. X) -> ((uAr) < if(p <_ q, p, q) -> ((uAr) < p /\ (uAr) < q)))
60		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = u -> (F` w) = (F` u))
61		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = u -> (G` w) = (G` u))
62	60, 61	opeq12d 3166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = u -> <.(F` w), (G` w)>. = <.(F` u), (G` u)>.)
63		opex 3527	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- <.(F` u), (G` u)>. e. _V
64	62, 34, 63	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u e. X -> (H` u) = <.(F` u), (G` u)>.)
65		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = r -> (F` w) = (F` r))
66		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (w = r -> (G` w) = (G` r))
67	65, 66	opeq12d 3166	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w = r -> <.(F` w), (G` w)>. = <.(F` r), (G` r)>.)
68		opex 3527	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- <.(F` r), (G` r)>. e. _V
69	67, 34, 68	fvopab4 4743	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (r e. X -> (H` r) = <.(F` r), (G` r)>.)
70	64, 69	opreqan12d 4902	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((u e. X /\ r e. X) -> ((H` u)D(H` r)) = (<.(F` u), (G` u)>.D<.(F` r), (G` r)>.))
71	70	adantl 424	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((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)>.))
72		opelxpi 4040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` u) e. Y /\ (G` u) e. Z) -> <.(F` u), (G` u)>. e. (Y X. Z))
73		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((F:X-->Y /\ u e. X) -> (F` u) e. Y)
74	73, 22	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F e. (J Cn K) /\ u e. X) -> (F` u) e. Y)
75		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((G:X-->Z /\ u e. X) -> (G` u) e. Z)
76	75, 27	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((G e. (J Cn L) /\ u e. X) -> (G` u) e. Z)
77	72, 74, 76	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. (J Cn K) /\ u e. X) /\ (G e. (J Cn L) /\ u e. X)) -> <.(F` u), (G` u)>. e. (Y X. Z))
78	77	anandirs 571	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ u e. X) -> <.(F` u), (G` u)>. e. (Y X. Z))
79	78	adantrr 431	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ r e. X)) -> <.(F` u), (G` u)>. e. (Y X. Z))
80		opelxpi 4040	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F` r) e. Y /\ (G` r) e. Z) -> <.(F` r), (G` r)>. e. (Y X. Z))
81		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((F:X-->Y /\ r e. X) -> (F` r) e. Y)
82	81, 22	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F e. (J Cn K) /\ r e. X) -> (F` r) e. Y)
83		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((G:X-->Z /\ r e. X) -> (G` r) e. Z)
84	83, 27	sylan 497	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((G e. (J Cn L) /\ r e. X) -> (G` r) e. Z)
85	80, 82, 84	syl2an 503	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. (J Cn K) /\ r e. X) /\ (G e. (J Cn L) /\ r e. X)) -> <.(F` r), (G` r)>. e. (Y X. Z))
86	85	anandirs 571	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ r e. X) -> <.(F` r), (G` r)>. e. (Y X. Z))
87	86	adantrl 430	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F e. (J Cn K) /\ G e. (J Cn L)) /\ (u e. X /\ r e. X)) -> <.(F` r), (G` r)>. e. (Y X. Z))
88		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F` u) e. _V
89	88	op1st 5026	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (1st` <.(F` u), (G` u)>.) = (F` u)
90	89	eqcomi 1888	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F` u) = (1st` <.(F` u), (G` u)>.)
91		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (G` u) e. _V
92	88, 91	op2nd 5027	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (2nd` <.(F` u), (G` u)>.) = (G` u)
93	92	eqcomi 1888	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (G` u) = (2nd` <.(F` u), (G` u)>.)
94		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F` r) e. _V
95	94	op1st 5026	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (1st` <.(F` r), (G` r)>.) = (F` r)
96	95	eqcomi 1888	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F` r) = (1st` <.(F` r), (G` r)>.)
97		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (G` r) e. _V
98	94, 97	op2nd 5027	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (2nd` <.(F` r), (G` r)>.) = (G` r)
99	98	eqcomi 1888	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (G` r) = (2nd` <.(F` r), (G` r)>.)
100	2, 3, 4, 5, 6, 90, 93, 96, 99	metxpdval 9106	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((<.(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))))
101	79, 87, 100	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((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))))
102	71, 101	eqtrd 1925	. . . . . . . . . . . . . . . . . . . . . 22 |- (((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))))
103	102	breq1d 3348	. . . . . . . . . . . . . . . . . . . . 21 |- (((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))
104		breq1 3341	. . . . . . . . . . . . . . . . . . . . . 22 |- (((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))
105		breq1 3341	. . . . . . . . . . . . . . . . . . . . . 22 |- (((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))
106	104, 105	ifboth 3002	. . . . . . . . . . . . . . . . . . . . 21 |- ((((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)
107	103, 106	syl5bir 227	. . . . . . . . . . . . . . . . . . . 20 |- (((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))
108	107	anassrs 489	. . . . . . . . . . . . . . . . . . 19 |- ((((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))
109		simp1 876	. . . . . . . . . . . . . . . . . . 19 |- ((u e. X /\ t e. RR /\ 0 < t) -> u e. X)
110	108, 109	sylanl2 510	. . . . . . . . . . . . . . . . . 18 |- ((((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))
111	110	adantlr 429	. . . . . . . . . . . . . . . . 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)) /\ r e. X) -> ((((F` u)B(F` r)) < t /\ ((G` u)C(G` r)) < t) -> ((H` u)D(H` r)) < t))
112	59, 111	imim12d 69	. . . . . . . . . . . . . . . 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)) /\ 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)))
113	112	adantlr 429	. . . . . . . . . . . . . . 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)) /\ 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)))
114		prth 615	. . . . . . . . . . . . . . 15 |- ((((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)))
115	113, 114	syl5 20	. . . . . . . . . . . . . 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)) /\ 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)))
116	115	ralimdvaa 2171	. . . . . . . . . . . . 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)) -> A.r e. X ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t)))
117	116	impr 422	. . . . . . . . . . . 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)))) -> A.r e. X ((uAr) < if(p <_ q, p, q) -> ((H` u)D(H` r)) < t))
118		breq2 3342	. . . . . . . . . . . . . 14 |- (s = if(p <_ q, p, q) -> (0 < s <-> 0 < if(p <_ q, p, q)))
119		breq2 3342	. . . . . . . . . . . . . . . 16 |- (s = if(p <_ q, p, q) -> ((uAr) < s <-> (uAr) < if(p <_ q, p, q)))
120	119	imbi1d 675	. . . . . . . . . . . . . . 15 |- (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)))
121	120	ralbidv 2123	. . . . . . . . . . . . . 14 |- (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)))
122	118, 121	anbi12d 690	. . . . . . . . . . . . 13 |- (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))))
123	122	rcla4ev 2381	. . . . . . . . . . . 12 |- ((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)))
124	46, 50, 117, 123	syl12anc 1098	. . . . . . . . . . 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)))
125	124	ex 402	. . . . . . . . . 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 /\ 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))))
126		an4 564	. . . . . . . . . . 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) /\ A.r e. X ((uAr) < q -> ((G` u)C(G` r)) < t))))
127		r19.26 2219	. . . . . . . . . . . 12 |- (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)))
128	127	anbi2i 538	. . . . . . . . . . 11 |- (((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))))
129	126, 128	bitr4i 193	. . . . . . . . . 10 |- (((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))))
130	125, 129	syl5ib 223	. . . . . . . . 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))))
131	130	ex 402	. . . . . . . 8 |- (((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)))))
132	131	r19.23advv 2218	. . . . . . 7 |- (((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))))
133		reeanv 2249	. . . . . . 7 |- (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))))
134	132, 133	syl5ibr 224	. . . . . 6 |- (((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))))
135	40, 44, 134	mp2and 767	. . . . 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)))
136	135	3exp2 1086	. . . 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))))))
137	136	imp3a 388	. . 3 |- ((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)))))
138	137	r19.21aivv 2183	. 2 |- ((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))))
139	18, 36, 138	sylanbrc 527	1 |- ((F e. (J Cn K) /\ G e. (J Cn L)) -> H e. (J Cn M))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  ifcif 2982  {cpr 3045  <.cop 3046   class class class wbr 3338  {copab 3395   X. cxp 3984  dom cdm 3986  -->wf 3994  ` cfv 3998  (class class class)co 4884  {copab2 4885  1stc1st 5018  2ndc2nd 5019  supcsup 5663  RRcr 6385  0cc0 6386   <_ cle 6448   < clt 6653   Cn ccn 9028  Metcme 9066  Opencopn 9069

This theorem is referenced by:  oprcn 9255

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-sup 5664  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-2 7154  df-top 8861  df-cn 9030  df-cnp 9031  df-met 9070  df-bl 9072  df-opn 9073

Copyright terms: Public domain