Theorem xpcn 7973

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 ∈ Met
xpcn.8	⊢ B ∈ Met
xpcn.9	⊢ C ∈ Met
xpcn.10	⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (Y × Z) ⋀ y ∈ (Y × Z)) ⋀ z = sup({((1st ‘x)B(1st ‘y)), ((2nd ‘x)C(2nd ‘y))}, ℝ, < ))}
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 ∈ X ⋀ v = ⟨(F ‘w), (G ‘w)⟩)}

Assertion

Ref	Expression
xpcn	⊢ ((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) → H ∈ (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 3820	. . . . . . . . 9 ⊢ ((F:X–→Y ⋀ w ∈ X) → (F ‘w) ∈ Y)
2		xpcn.7	. . . . . . . . . 10 ⊢ A ∈ Met
3		xpcn.8	. . . . . . . . . 10 ⊢ B ∈ 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 7881	. . . . . . . . . 10 ⊢ ((A ∈ Met ⋀ B ∈ Met ⋀ F ∈ (J Cn K)) → F:X–→Y)
9	2, 3, 8	mp3an12 908	. . . . . . . . 9 ⊢ (F ∈ (J Cn K) → F:X–→Y)
10	1, 9	sylan 450	. . . . . . . 8 ⊢ ((F ∈ (J Cn K) ⋀ w ∈ X) → (F ‘w) ∈ Y)
11		ffvelrn 3820	. . . . . . . . 9 ⊢ ((G:X–→Z ⋀ w ∈ X) → (G ‘w) ∈ Z)
12		xpcn.9	. . . . . . . . . 10 ⊢ C ∈ Met
13		xpcn.5	. . . . . . . . . . 11 ⊢ Z = dom dom C
14		xpcn.11a	. . . . . . . . . . 11 ⊢ L = (Open ‘C)
15	4, 13, 6, 14	metcnf 7881	. . . . . . . . . 10 ⊢ ((A ∈ Met ⋀ C ∈ Met ⋀ G ∈ (J Cn L)) → G:X–→Z)
16	2, 12, 15	mp3an12 908	. . . . . . . . 9 ⊢ (G ∈ (J Cn L) → G:X–→Z)
17	11, 16	sylan 450	. . . . . . . 8 ⊢ ((G ∈ (J Cn L) ⋀ w ∈ X) → (G ‘w) ∈ Z)
18	10, 17	anim12i 333	. . . . . . 7 ⊢ (((F ∈ (J Cn K) ⋀ w ∈ X) ⋀ (G ∈ (J Cn L) ⋀ w ∈ X)) → ((F ‘w) ∈ Y ⋀ (G ‘w) ∈ Z))
19	18	anandirs 515	. . . . . 6 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ w ∈ X) → ((F ‘w) ∈ Y ⋀ (G ‘w) ∈ Z))
20		opelxpi 3223	. . . . . 6 ⊢ (((F ‘w) ∈ Y ⋀ (G ‘w) ∈ Z) → ⟨(F ‘w), (G ‘w)⟩ ∈ (Y × Z))
21	19, 20	syl 10	. . . . 5 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ w ∈ X) → ⟨(F ‘w), (G ‘w)⟩ ∈ (Y × Z))
22	21	r19.21aiva 1717	. . . 4 ⊢ ((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) → ∀w ∈ X ⟨(F ‘w), (G ‘w)⟩ ∈ (Y × Z))
23		xpcn.13	. . . . 5 ⊢ H = {⟨w, v⟩∣(w ∈ X ⋀ v = ⟨(F ‘w), (G ‘w)⟩)}
24	23	fopab2 3829	. . . 4 ⊢ (∀w ∈ X ⟨(F ‘w), (G ‘w)⟩ ∈ (Y × Z) ↔ H:X–→(Y × Z))
25	22, 24	sylib 198	. . 3 ⊢ ((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) → H:X–→(Y × Z))
26	4, 6, 5, 7	metcni 7891	. . . . . . . . . 10 ⊢ (((A ∈ Met ⋀ B ∈ Met ⋀ F ∈ (J Cn K)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) → ∃p ∈ ℝ (0 < p ⋀ ∀r ∈ X ((uAr) < p → ((F ‘u)B(F ‘r)) < t)))
27	2, 26	mp3anl1 912	. . . . . . . . 9 ⊢ (((B ∈ Met ⋀ F ∈ (J Cn K)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) → ∃p ∈ ℝ (0 < p ⋀ ∀r ∈ X ((uAr) < p → ((F ‘u)B(F ‘r)) < t)))
28	3, 27	mpanl1 708	. . . . . . . 8 ⊢ ((F ∈ (J Cn K) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) → ∃p ∈ ℝ (0 < p ⋀ ∀r ∈ X ((uAr) < p → ((F ‘u)B(F ‘r)) < t)))
29	28	adantlr 395	. . . . . . 7 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) → ∃p ∈ ℝ (0 < p ⋀ ∀r ∈ X ((uAr) < p → ((F ‘u)B(F ‘r)) < t)))
30	4, 6, 13, 14	metcni 7891	. . . . . . . . . 10 ⊢ (((A ∈ Met ⋀ C ∈ Met ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) → ∃q ∈ ℝ (0 < q ⋀ ∀r ∈ X ((uAr) < q → ((G ‘u)C(G ‘r)) < t)))
31	2, 30	mp3anl1 912	. . . . . . . . 9 ⊢ (((C ∈ Met ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) → ∃q ∈ ℝ (0 < q ⋀ ∀r ∈ X ((uAr) < q → ((G ‘u)C(G ‘r)) < t)))
32	12, 31	mpanl1 708	. . . . . . . 8 ⊢ ((G ∈ (J Cn L) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) → ∃q ∈ ℝ (0 < q ⋀ ∀r ∈ X ((uAr) < q → ((G ‘u)C(G ‘r)) < t)))
33	32	adantll 394	. . . . . . 7 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) → ∃q ∈ ℝ (0 < q ⋀ ∀r ∈ X ((uAr) < q → ((G ‘u)C(G ‘r)) < t)))
34		breq2 2628	. . . . . . . . . . . . . . 15 ⊢ (s = if(p ≤ q, p, q) → (0 < s ↔ 0 < if(p ≤ q, p, q)))
35		breq2 2628	. . . . . . . . . . . . . . . . 17 ⊢ (s = if(p ≤ q, p, q) → ((uAr) < s ↔ (uAr) < if(p ≤ q, p, q)))
36	35	imbi1d 615	. . . . . . . . . . . . . . . 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 1666	. . . . . . . . . . . . . . 15 ⊢ (s = if(p ≤ q, p, q) → (∀r ∈ X ((uAr) < s → ((H ‘u)D(H ‘r)) < t) ↔ ∀r ∈ X ((uAr) < if(p ≤ q, p, q) → ((H ‘u)D(H ‘r)) < t)))
38	34, 37	anbi12d 630	. . . . . . . . . . . . . 14 ⊢ (s = if(p ≤ q, p, q) → ((0 < s ⋀ ∀r ∈ X ((uAr) < s → ((H ‘u)D(H ‘r)) < t)) ↔ (0 < if(p ≤ q, p, q) ⋀ ∀r ∈ X ((uAr) < if(p ≤ q, p, q) → ((H ‘u)D(H ‘r)) < t))))
39	38	rcla4ev 1880	. . . . . . . . . . . . 13 ⊢ (( if(p ≤ q, p, q) ∈ ℝ ⋀ (0 < if(p ≤ q, p, q) ⋀ ∀r ∈ X ((uAr) < if(p ≤ q, p, q) → ((H ‘u)D(H ‘r)) < t))) → ∃s ∈ ℝ (0 < s ⋀ ∀r ∈ X ((uAr) < s → ((H ‘u)D(H ‘r)) < t)))
40		ifcl 2384	. . . . . . . . . . . . . 14 ⊢ ((p ∈ ℝ ⋀ q ∈ ℝ) → if(p ≤ q, p, q) ∈ ℝ)
41	40	ad2antlr 407	. . . . . . . . . . . . 13 ⊢ (((((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) ⋀ (p ∈ ℝ ⋀ q ∈ ℝ)) ⋀ ((0 < p ⋀ 0 < q) ⋀ ∀r ∈ X (((uAr) < p → ((F ‘u)B(F ‘r)) < t) ⋀ ((uAr) < q → ((G ‘u)C(G ‘r)) < t)))) → if(p ≤ q, p, q) ∈ ℝ)
42		breq2 2628	. . . . . . . . . . . . . . . 16 ⊢ (p = if(p ≤ q, p, q) → (0 < p ↔ 0 < if(p ≤ q, p, q)))
43		breq2 2628	. . . . . . . . . . . . . . . 16 ⊢ (q = if(p ≤ q, p, q) → (0 < q ↔ 0 < if(p ≤ q, p, q)))
44	42, 43	ifboth 2379	. . . . . . . . . . . . . . 15 ⊢ ((0 < p ⋀ 0 < q) → 0 < if(p ≤ q, p, q))
45	44	ad2antrl 408	. . . . . . . . . . . . . 14 ⊢ (((((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) ⋀ (p ∈ ℝ ⋀ q ∈ ℝ)) ⋀ ((0 < p ⋀ 0 < q) ⋀ ∀r ∈ X (((uAr) < p → ((F ‘u)B(F ‘r)) < t) ⋀ ((uAr) < q → ((G ‘u)C(G ‘r)) < t)))) → 0 < if(p ≤ q, p, q))
46		ltmint 5925	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((uAr) ∈ ℝ ⋀ p ∈ ℝ ⋀ q ∈ ℝ) → ((uAr) < if(p ≤ q, p, q) ↔ ((uAr) < p ⋀ (uAr) < q)))
47	46	biimpd 153	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((uAr) ∈ ℝ ⋀ p ∈ ℝ ⋀ q ∈ ℝ) → ((uAr) < if(p ≤ q, p, q) → ((uAr) < p ⋀ (uAr) < q)))
48	4	metcl 7808	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((A ∈ Met ⋀ u ∈ X ⋀ r ∈ X) → (uAr) ∈ ℝ)
49	2, 48	mp3an1 905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((u ∈ X ⋀ r ∈ X) → (uAr) ∈ ℝ)
50	49	3ad2antl1 811	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t) ⋀ r ∈ X) → (uAr) ∈ ℝ)
51	47, 50	syl3an1 861	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t) ⋀ r ∈ X) ⋀ p ∈ ℝ ⋀ q ∈ ℝ) → ((uAr) < if(p ≤ q, p, q) → ((uAr) < p ⋀ (uAr) < q)))
52	51	3expb 836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t) ⋀ r ∈ X) ⋀ (p ∈ ℝ ⋀ q ∈ ℝ)) → ((uAr) < if(p ≤ q, p, q) → ((uAr) < p ⋀ (uAr) < q)))
53	52	an1rs 491	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t) ⋀ (p ∈ ℝ ⋀ q ∈ ℝ)) ⋀ r ∈ X) → ((uAr) < if(p ≤ q, p, q) → ((uAr) < p ⋀ (uAr) < q)))
54	53	adantlll 398	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) ⋀ (p ∈ ℝ ⋀ q ∈ ℝ)) ⋀ r ∈ X) → ((uAr) < if(p ≤ q, p, q) → ((uAr) < p ⋀ (uAr) < q)))
55		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (w = u → (F ‘w) = (F ‘u))
56		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (w = u → (G ‘w) = (G ‘u))
57	55, 56	opeq12d 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (w = u → ⟨(F ‘w), (G ‘w)⟩ = ⟨(F ‘u), (G ‘u)⟩)
58		opex 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ⟨(F ‘u), (G ‘u)⟩ ∈ V
59	57, 23, 58	fvopab4 3786	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (u ∈ X → (H ‘u) = ⟨(F ‘u), (G ‘u)⟩)
60		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (w = r → (F ‘w) = (F ‘r))
61		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (w = r → (G ‘w) = (G ‘r))
62	60, 61	opeq12d 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (w = r → ⟨(F ‘w), (G ‘w)⟩ = ⟨(F ‘r), (G ‘r)⟩)
63		opex 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ⟨(F ‘r), (G ‘r)⟩ ∈ V
64	62, 23, 63	fvopab4 3786	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (r ∈ X → (H ‘r) = ⟨(F ‘r), (G ‘r)⟩)
65	59, 64	opreqan12d 3985	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((u ∈ X ⋀ r ∈ X) → ((H ‘u)D(H ‘r)) = (⟨(F ‘u), (G ‘u)⟩D⟨(F ‘r), (G ‘r)⟩))
66	65	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ r ∈ X)) → ((H ‘u)D(H ‘r)) = (⟨(F ‘u), (G ‘u)⟩D⟨(F ‘r), (G ‘r)⟩))
67		xpcn.10	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (Y × Z) ⋀ y ∈ (Y × Z)) ⋀ z = sup({((1st ‘x)B(1st ‘y)), ((2nd ‘x)C(2nd ‘y))}, ℝ, < ))}
68		fvex 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (F ‘u) ∈ V
69	68	op1st 4091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (1st ‘⟨(F ‘u), (G ‘u)⟩) = (F ‘u)
70	69	eqcomi 1482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (F ‘u) = (1st ‘⟨(F ‘u), (G ‘u)⟩)
71		fvex 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (G ‘u) ∈ V
72	68, 71	op2nd 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (2nd ‘⟨(F ‘u), (G ‘u)⟩) = (G ‘u)
73	72	eqcomi 1482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (G ‘u) = (2nd ‘⟨(F ‘u), (G ‘u)⟩)
74		fvex 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (F ‘r) ∈ V
75	74	op1st 4091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (1st ‘⟨(F ‘r), (G ‘r)⟩) = (F ‘r)
76	75	eqcomi 1482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (F ‘r) = (1st ‘⟨(F ‘r), (G ‘r)⟩)
77		fvex 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (G ‘r) ∈ V
78	74, 77	op2nd 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (2nd ‘⟨(F ‘r), (G ‘r)⟩) = (G ‘r)
79	78	eqcomi 1482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (G ‘r) = (2nd ‘⟨(F ‘r), (G ‘r)⟩)
80	5, 13, 3, 12, 67, 70, 73, 76, 79	metxpdval 7826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨(F ‘u), (G ‘u)⟩ ∈ (Y × Z) ⋀ ⟨(F ‘r), (G ‘r)⟩ ∈ (Y × 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 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((F ‘u) ∈ Y ⋀ (G ‘u) ∈ Z) → ⟨(F ‘u), (G ‘u)⟩ ∈ (Y × Z))
82		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((F:X–→Y ⋀ u ∈ X) → (F ‘u) ∈ Y)
83	82, 9	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((F ∈ (J Cn K) ⋀ u ∈ X) → (F ‘u) ∈ Y)
84		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((G:X–→Z ⋀ u ∈ X) → (G ‘u) ∈ Z)
85	84, 16	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((G ∈ (J Cn L) ⋀ u ∈ X) → (G ‘u) ∈ Z)
86	81, 83, 85	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((F ∈ (J Cn K) ⋀ u ∈ X) ⋀ (G ∈ (J Cn L) ⋀ u ∈ X)) → ⟨(F ‘u), (G ‘u)⟩ ∈ (Y × Z))
87	86	anandirs 515	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ u ∈ X) → ⟨(F ‘u), (G ‘u)⟩ ∈ (Y × Z))
88	87	adantrr 397	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ r ∈ X)) → ⟨(F ‘u), (G ‘u)⟩ ∈ (Y × Z))
89		opelxpi 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((F ‘r) ∈ Y ⋀ (G ‘r) ∈ Z) → ⟨(F ‘r), (G ‘r)⟩ ∈ (Y × Z))
90		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((F:X–→Y ⋀ r ∈ X) → (F ‘r) ∈ Y)
91	90, 9	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((F ∈ (J Cn K) ⋀ r ∈ X) → (F ‘r) ∈ Y)
92		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((G:X–→Z ⋀ r ∈ X) → (G ‘r) ∈ Z)
93	92, 16	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((G ∈ (J Cn L) ⋀ r ∈ X) → (G ‘r) ∈ Z)
94	89, 91, 93	syl2an 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((F ∈ (J Cn K) ⋀ r ∈ X) ⋀ (G ∈ (J Cn L) ⋀ r ∈ X)) → ⟨(F ‘r), (G ‘r)⟩ ∈ (Y × Z))
95	94	anandirs 515	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ r ∈ X) → ⟨(F ‘r), (G ‘r)⟩ ∈ (Y × Z))
96	95	adantrl 396	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ r ∈ X)) → ⟨(F ‘r), (G ‘r)⟩ ∈ (Y × Z))
97	80, 88, 96	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ r ∈ 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 1510	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ r ∈ 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 2634	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ r ∈ 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 2627	. . . . . . . . . . . . . . . . . . . . . . . . 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 2627	. . . . . . . . . . . . . . . . . . . . . . . . 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 2379	. . . . . . . . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ r ∈ 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 ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ u ∈ X) ⋀ r ∈ X) → ((((F ‘u)B(F ‘r)) < t ⋀ ((G ‘u)C(G ‘r)) < t) → ((H ‘u)D(H ‘r)) < t))
105		3simp1 790	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t) → u ∈ X)
106	104, 105	sylanl2 463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) ⋀ r ∈ X) → ((((F ‘u)B(F ‘r)) < t ⋀ ((G ‘u)C(G ‘r)) < t) → ((H ‘u)D(H ‘r)) < t))
107	106	adantlr 395	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((F ∈ (J Cn K) ⋀ G ∈ (J Cn L)) ⋀ (u ∈ X ⋀ t ∈ ℝ ⋀ 0 < t)) ⋀ (p ∈ ℝ ⋀ q ∈ ℝ)) ⋀ r ∈ 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 ∈ (J Cn K) ⋀ G ∈ (J Cn