Theorem xplmi 7970

Description: Two sequences converge if the sequence of their ordered pairs converges. One direction of Proposition 14-2.6 of [Gleason] p. 230. Warning: The HTML proof page is 0.5MB in size.

Hypotheses

Ref	Expression
xplm.a	⊢ R ∈ V
xplm.b	⊢ S ∈ V
xplm.1	⊢ X = dom dom B
xplm.3	⊢ Y = dom dom C
xplm.5	⊢ B ∈ Met
xplm.6	⊢ C ∈ Met
xplm.7	⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (X × Y) ⋀ y ∈ (X × Y)) ⋀ z = sup({((1st ‘x)B(1st ‘y)), ((2nd ‘x)C(2nd ‘y))}, ℝ, < ))}
xplmi.9	⊢ F = {⟨k, w⟩∣(k ∈ ℕ ⋀ w = (1st ‘(H ‘k)))}
xplmi.10	⊢ G = {⟨k, w⟩∣(k ∈ ℕ ⋀ w = (2nd ‘(H ‘k)))}

Assertion

Ref	Expression
xplmi	⊢ ((H:ℕ–→(X × Y) ⋀ H(⇝m ‘D)⟨R, S⟩) → ((F:ℕ–→X ⋀ F(⇝m ‘B)R) ⋀ (G:ℕ–→Y ⋀ G(⇝m ‘C)S)))

Distinct variable groups:   x,y,z,B   x,C,y,z   x,R,y,z   x,S,y,z   w,k,x,y,z,X   k,Y,w,x,y,z   x,F,y,z   x,G,y,z   k,H,w

Proof of Theorem xplmi

Step	Hyp	Ref	Expression
1		simprl 416	. . . . . . . 8 ⊢ ((H(⇝m ‘D)⟨R, S⟩ ⋀ (R ∈ X ⋀ S ∈ Y)) → R ∈ X)
2	1	a1i 8	. . . . . . 7 ⊢ (H:ℕ–→(X × Y) → ((H(⇝m ‘D)⟨R, S⟩ ⋀ (R ∈ X ⋀ S ∈ Y)) → R ∈ X))
3		opex 2788	. . . . . . . . . . . . 13 ⊢ ⟨R, S⟩ ∈ V
4		xplm.1	. . . . . . . . . . . . . . 15 ⊢ X = dom dom B
5		xplm.3	. . . . . . . . . . . . . . 15 ⊢ Y = dom dom C
6		xplm.5	. . . . . . . . . . . . . . 15 ⊢ B ∈ Met
7		xplm.6	. . . . . . . . . . . . . . 15 ⊢ C ∈ Met
8		xplm.7	. . . . . . . . . . . . . . 15 ⊢ D = {⟨⟨x, y⟩, z⟩∣((x ∈ (X × Y) ⋀ y ∈ (X × Y)) ⋀ z = sup({((1st ‘x)B(1st ‘y)), ((2nd ‘x)C(2nd ‘y))}, ℝ, < ))}
9	4, 5, 6, 7, 8	metxp 7831	. . . . . . . . . . . . . 14 ⊢ D ∈ Met
10		ltso 5524	. . . . . . . . . . . . . . . . . . 19 ⊢ < Or ℝ
11	10	supex 4586	. . . . . . . . . . . . . . . . . 18 ⊢ sup({((1st ‘x)B(1st ‘y)), ((2nd ‘x)C(2nd ‘y))}, ℝ, < ) ∈ V
12	11, 8	dmoprab2 4129	. . . . . . . . . . . . . . . . 17 ⊢ dom D = ((X × Y) × (X × Y))
13	12	dmeqi 3318	. . . . . . . . . . . . . . . 16 ⊢ dom dom D = dom ((X × Y) × (X × Y))
14		dmxpid 3339	. . . . . . . . . . . . . . . 16 ⊢ dom ((X × Y) × (X × Y)) = (X × Y)
15	13, 14	eqtr2 1499	. . . . . . . . . . . . . . 15 ⊢ (X × Y) = dom dom D
16		1z 6161	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℤ
17		nnuz 6440	. . . . . . . . . . . . . . 15 ⊢ ℕ = (ℤ≥ ‘1)
18	15, 16, 17	lmcvg2 7930	. . . . . . . . . . . . . 14 ⊢ (((D ∈ Met ⋀ ⟨R, S⟩ ∈ V ⋀ H(⇝m ‘D)⟨R, S⟩) ⋀ (v ∈ ℝ ⋀ 0 < v)) → ∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((H ‘m)D⟨R, S⟩) < v))
19	9, 18	mp3anl1 912	. . . . . . . . . . . . 13 ⊢ (((⟨R, S⟩ ∈ V ⋀ H(⇝m ‘D)⟨R, S⟩) ⋀ (v ∈ ℝ ⋀ 0 < v)) → ∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((H ‘m)D⟨R, S⟩) < v))
20	3, 19	mpanl1 708	. . . . . . . . . . . 12 ⊢ ((H(⇝m ‘D)⟨R, S⟩ ⋀ (v ∈ ℝ ⋀ 0 < v)) → ∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((H ‘m)D⟨R, S⟩) < v))
21	20	adantlr 395	. . . . . . . . . . 11 ⊢ (((H(⇝m ‘D)⟨R, S⟩ ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ (v ∈ ℝ ⋀ 0 < v)) → ∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((H ‘m)D⟨R, S⟩) < v))
22	21	adantll 394	. . . . . . . . . 10 ⊢ (((H:ℕ–→(X × Y) ⋀ (H(⇝m ‘D)⟨R, S⟩ ⋀ (R ∈ X ⋀ S ∈ Y))) ⋀ (v ∈ ℝ ⋀ 0 < v)) → ∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((H ‘m)D⟨R, S⟩) < v))
23		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) → (H ‘m) ∈ (X × Y))
24		elxp6 4108	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((H ‘m) ∈ (X × Y) ↔ ((H ‘m) = ⟨(1st ‘(H ‘m)), (2nd ‘(H ‘m))⟩ ⋀ ((1st ‘(H ‘m)) ∈ X ⋀ (2nd ‘(H ‘m)) ∈ Y)))
25	24	pm3.26bi 322	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((H ‘m) ∈ (X × Y) → (H ‘m) = ⟨(1st ‘(H ‘m)), (2nd ‘(H ‘m))⟩)
26	23, 25	syl 10	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) → (H ‘m) = ⟨(1st ‘(H ‘m)), (2nd ‘(H ‘m))⟩)
27		fveq2 3730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (k = m → (H ‘k) = (H ‘m))
28	27	fveq2d 3734	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (k = m → (1st ‘(H ‘k)) = (1st ‘(H ‘m)))
29		xplmi.9	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ F = {⟨k, w⟩∣(k ∈ ℕ ⋀ w = (1st ‘(H ‘k)))}
30		fvex 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (1st ‘(H ‘m)) ∈ V
31	28, 29, 30	fvopab4 3786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (m ∈ ℕ → (F ‘m) = (1st ‘(H ‘m)))
32	27	fveq2d 3734	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (k = m → (2nd ‘(H ‘k)) = (2nd ‘(H ‘m)))
33		xplmi.10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ G = {⟨k, w⟩∣(k ∈ ℕ ⋀ w = (2nd ‘(H ‘k)))}
34		fvex 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2nd ‘(H ‘m)) ∈ V
35	32, 33, 34	fvopab4 3786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (m ∈ ℕ → (G ‘m) = (2nd ‘(H ‘m)))
36	31, 35	opeq12d 2499	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (m ∈ ℕ → ⟨(F ‘m), (G ‘m)⟩ = ⟨(1st ‘(H ‘m)), (2nd ‘(H ‘m))⟩)
37	36	adantl 390	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) → ⟨(F ‘m), (G ‘m)⟩ = ⟨(1st ‘(H ‘m)), (2nd ‘(H ‘m))⟩)
38	26, 37	eqtr4d 1513	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) → (H ‘m) = ⟨(F ‘m), (G ‘m)⟩)
39	38	opreq1d 3981	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) → ((H ‘m)D⟨R, S⟩) = (⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩))
40	39	breq1d 2634	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) → (((H ‘m)D⟨R, S⟩) < v ↔ (⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) < v))
41	40	adantr 391	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) → (((H ‘m)D⟨R, S⟩) < v ↔ (⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) < v))
42	5	metcl 7808	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((C ∈ Met ⋀ (G ‘m) ∈ Y ⋀ S ∈ Y) → ((G ‘m)CS) ∈ ℝ)
43	7, 42	mp3an1 905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((G ‘m) ∈ Y ⋀ S ∈ Y) → ((G ‘m)CS) ∈ ℝ)
44		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((G:ℕ–→Y ⋀ m ∈ ℕ) → (G ‘m) ∈ Y)
45		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((H:ℕ–→(X × Y) ⋀ k ∈ ℕ) → (H ‘k) ∈ (X × Y))
46		elxp7 4109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((H ‘k) ∈ (X × Y) ↔ ((H ‘k) ∈ (V × V) ⋀ ((1st ‘(H ‘k)) ∈ X ⋀ (2nd ‘(H ‘k)) ∈ Y)))
47	46	pm3.27bi 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((H ‘k) ∈ (X × Y) → ((1st ‘(H ‘k)) ∈ X ⋀ (2nd ‘(H ‘k)) ∈ Y))
48	47	pm3.27d 325	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((H ‘k) ∈ (X × Y) → (2nd ‘(H ‘k)) ∈ Y)
49	45, 48	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((H:ℕ–→(X × Y) ⋀ k ∈ ℕ) → (2nd ‘(H ‘k)) ∈ Y)
50	49	r19.21aiva 1717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (H:ℕ–→(X × Y) → ∀k ∈ ℕ (2nd ‘(H ‘k)) ∈ Y)
51	33	fopab2 3829	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀k ∈ ℕ (2nd ‘(H ‘k)) ∈ Y ↔ G:ℕ–→Y)
52	50, 51	sylib 198	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (H:ℕ–→(X × Y) → G:ℕ–→Y)
53	44, 52	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) → (G ‘m) ∈ Y)
54	43, 53	sylan 450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ S ∈ Y) → ((G ‘m)CS) ∈ ℝ)
55	54	adantrl 396	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ (R ∈ X ⋀ S ∈ Y)) → ((G ‘m)CS) ∈ ℝ)
56	55	adantrr 397	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) → ((G ‘m)CS) ∈ ℝ)
57	4	metcl 7808	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((B ∈ Met ⋀ (F ‘m) ∈ X ⋀ R ∈ X) → ((F ‘m)BR) ∈ ℝ)
58	6, 57	mp3an1 905	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((F ‘m) ∈ X ⋀ R ∈ X) → ((F ‘m)BR) ∈ ℝ)
59		ffvelrn 3820	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((F:ℕ–→X ⋀ m ∈ ℕ) → (F ‘m) ∈ X)
60	47	pm3.26d 321	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((H ‘k) ∈ (X × Y) → (1st ‘(H ‘k)) ∈ X)
61	45, 60	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((H:ℕ–→(X × Y) ⋀ k ∈ ℕ) → (1st ‘(H ‘k)) ∈ X)
62	61	r19.21aiva 1717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (H:ℕ–→(X × Y) → ∀k ∈ ℕ (1st ‘(H ‘k)) ∈ X)
63	29	fopab2 3829	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀k ∈ ℕ (1st ‘(H ‘k)) ∈ X ↔ F:ℕ–→X)
64	62, 63	sylib 198	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (H:ℕ–→(X × Y) → F:ℕ–→X)
65	59, 64	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) → (F ‘m) ∈ X)
66	58, 65	sylan 450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ R ∈ X) → ((F ‘m)BR) ∈ ℝ)
67	66	adantrr 397	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ (R ∈ X ⋀ S ∈ Y)) → ((F ‘m)BR) ∈ ℝ)
68	67	adantrr 397	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) → ((F ‘m)BR) ∈ ℝ)
69		fvex 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (F ‘m) ∈ V
70	69	op1st 4091	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (1st ‘⟨(F ‘m), (G ‘m)⟩) = (F ‘m)
71	70	eqcomi 1482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (F ‘m) = (1st ‘⟨(F ‘m), (G ‘m)⟩)
72		fvex 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (G ‘m) ∈ V
73	69, 72	op2nd 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2nd ‘⟨(F ‘m), (G ‘m)⟩) = (G ‘m)
74	73	eqcomi 1482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (G ‘m) = (2nd ‘⟨(F ‘m), (G ‘m)⟩)
75		xplm.a	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ R ∈ V
76	75	op1st 4091	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (1st ‘⟨R, S⟩) = R
77	76	eqcomi 1482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ R = (1st ‘⟨R, S⟩)
78		xplm.b	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ S ∈ V
79	75, 78	op2nd 4092	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2nd ‘⟨R, S⟩) = S
80	79	eqcomi 1482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ S = (2nd ‘⟨R, S⟩)
81	4, 5, 6, 7, 8, 71, 74, 77, 80	metxptval 7827	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((⟨(F ‘m), (G ‘m)⟩ ∈ (X × Y) ⋀ ⟨R, S⟩ ∈ (X × Y)) ⋀ ((G ‘m)CS) ≤ ((F ‘m)BR)) → (⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) = ((F ‘m)BR))
82		opelxpi 3223	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((F ‘m) ∈ X ⋀ (G ‘m) ∈ Y) → ⟨(F ‘m), (G ‘m)⟩ ∈ (X × Y))
83	82, 65, 53	sylanc 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) → ⟨(F ‘m), (G ‘m)⟩ ∈ (X × Y))
84		opelxpi 3223	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((R ∈ X ⋀ S ∈ Y) → ⟨R, S⟩ ∈ (X × Y))
85	83, 84	anim12i 333	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ (R ∈ X ⋀ S ∈ Y)) → (⟨(F ‘m), (G ‘m)⟩ ∈ (X × Y) ⋀ ⟨R, S⟩ ∈ (X × Y)))
86	81, 85	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ ((G ‘m)CS) ≤ ((F ‘m)BR)) → (⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) = ((F ‘m)BR))
87	86	breq1d 2634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ ((G ‘m)CS) ≤ ((F ‘m)BR)) → ((⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) < v ↔ ((F ‘m)BR) < v))
88	87	biimpd 153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ ((G ‘m)CS) ≤ ((F ‘m)BR)) → ((⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) < v → ((F ‘m)BR) < v))
89	88	adantlrr 401	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) ⋀ ((G ‘m)CS) ≤ ((F ‘m)BR)) → ((⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) < v → ((F ‘m)BR) < v))
90	4, 5, 6, 7, 8, 71, 74, 77, 80	metxpfval 7828	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((⟨(F ‘m), (G ‘m)⟩ ∈ (X × Y) ⋀ ⟨R, S⟩ ∈ (X × Y)) ⋀ ((F ‘m)BR) ≤ ((G ‘m)CS)) → (⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) = ((G ‘m)CS))
91	90, 85	sylan 450	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ ((F ‘m)BR) ≤ ((G ‘m)CS)) → (⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) = ((G ‘m)CS))
92	91	adantlrr 401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) ⋀ ((F ‘m)BR) ≤ ((G ‘m)CS)) → (⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) = ((G ‘m)CS))
93	92	breq1d 2634	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) ⋀ ((F ‘m)BR) ≤ ((G ‘m)CS)) → ((⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) < v ↔ ((G ‘m)CS) < v))
94		lelttrt 5535	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((F ‘m)BR) ∈ ℝ ⋀ ((G ‘m)CS) ∈ ℝ ⋀ v ∈ ℝ) → ((((F ‘m)BR) ≤ ((G ‘m)CS) ⋀ ((G ‘m)CS) < v) → ((F ‘m)BR) < v))
95		simprr 417	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) → v ∈ ℝ)
96	94, 68, 56, 95	syl3anc 860	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) → ((((F ‘m)BR) ≤ ((G ‘m)CS) ⋀ ((G ‘m)CS) < v) → ((F ‘m)BR) < v))
97	96	expdimp 377	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) ⋀ ((F ‘m)BR) ≤ ((G ‘m)CS)) → (((G ‘m)CS) < v → ((F ‘m)BR) < v))
98	93, 97	sylbid 203	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) ⋀ ((F ‘m)BR) ≤ ((G ‘m)CS)) → ((⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) < v → ((F ‘m)BR) < v))
99	56, 68, 89, 98	lecase 5633	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) → ((⟨(F ‘m), (G ‘m)⟩D⟨R, S⟩) < v → ((F ‘m)BR) < v))
100	41, 99	sylbid 203	. . . . . . . . . . . . . . . . . . 19 ⊢ (((H:ℕ–→(X × Y) ⋀ m ∈ ℕ) ⋀ ((R ∈ X ⋀ S ∈ Y) ⋀ v ∈ ℝ)) → (((H ‘m)D⟨R, S⟩) < v → ((F ‘m)BR) < v))
101	100	exp43 386	. . . . . . . . . . . . . . . . . 18 ⊢ (H:ℕ–→(X × Y) → (m ∈ ℕ → ((R ∈ X ⋀ S ∈ Y) → (v ∈ ℝ → (((H ‘m)D⟨R, S⟩) < v → ((F ‘m)BR) < v)))))
102	101	com12 11	. . . . . . . . . . . . . . . . 17 ⊢ (m ∈ ℕ → (H:ℕ–→(X × Y) → ((R ∈ X ⋀ S ∈ Y) → (v ∈ ℝ → (((H ‘m)D⟨R, S⟩) < v → ((F ‘m)BR) < v)))))
103	102	com4l 39	. . . . . . . . . . . . . . . 16 ⊢ (H:ℕ–→(X × Y) → ((R ∈ X ⋀ S ∈ Y) → (v ∈ ℝ → (m ∈ ℕ → (((H ‘m)D⟨R, S⟩) < v → ((F ‘m)BR) < v)))))
104	103	imp41 368	. . . . . . . . . . . . . . 15 ⊢ ((((H:ℕ–→(X × Y) ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ v ∈ ℝ) ⋀ m ∈ ℕ) → (((H ‘m)D⟨R, S⟩) < v → ((F ‘m)BR) < v))
105	104	imim2d 25	. . . . . . . . . . . . . 14 ⊢ ((((H:ℕ–→(X × Y) ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ v ∈ ℝ) ⋀ m ∈ ℕ) → ((j ≤ m → ((H ‘m)D⟨R, S⟩) < v) → (j ≤ m → ((F ‘m)BR) < v)))
106	105	r19.20dva 1712	. . . . . . . . . . . . 13 ⊢ (((H:ℕ–→(X × Y) ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ v ∈ ℝ) → (∀m ∈ ℕ (j ≤ m → ((H ‘m)D⟨R, S⟩) < v) → ∀m ∈ ℕ (j ≤ m → ((F ‘m)BR) < v)))
107	106	r19.22sdv 1741	. . . . . . . . . . . 12 ⊢ (((H:ℕ–→(X × Y) ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ v ∈ ℝ) → (∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((H ‘m)D⟨R, S⟩) < v) → ∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((F ‘m)BR) < v)))
108	107	adantrr 397	. . . . . . . . . . 11 ⊢ (((H:ℕ–→(X × Y) ⋀ (R ∈ X ⋀ S ∈ Y)) ⋀ (v ∈ ℝ ⋀ 0 < v)) → (∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((H ‘m)D⟨R, S⟩) < v) → ∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((F ‘m)BR) < v)))
109	108	adantlrl 400	. . . . . . . . . 10 ⊢ (((H:ℕ–→(X × Y) ⋀ (H(⇝m ‘D)⟨R, S⟩ ⋀ (R ∈ X ⋀ S ∈ Y))) ⋀ (v ∈ ℝ ⋀ 0 < v)) → (∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((H ‘m)D⟨R, S⟩) < v) → ∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((F ‘m)BR) < v)))
110	22, 109	mpd 26	. . . . . . . . 9 ⊢ (((H:ℕ–→(X × Y) ⋀ (H(⇝m ‘D)⟨R, S⟩ ⋀ (R ∈ X ⋀ S ∈ Y))) ⋀ (v ∈ ℝ ⋀ 0 < v)) → ∃j ∈ ℕ ∀m ∈ ℕ (j ≤ m → ((F ‘m)BR) < v))
111	110	exp43 386	. . . . . . . 8 ⊢ (