Theorem xplm 7975

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

Hypotheses

Ref	Expression
xplm.a	|- R e. V
xplm.b	|- S e. V
xplm.1	|- X = dom dom B
xplm.3	|- Y = dom dom C
xplm.5	|- B e. Met
xplm.6	|- C e. Met
xplm.7	|- D = {<.<.x, y>., z>. | ((x e. (X X. Y) /\ y e. (X X. Y)) /\ z = sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ))}
xplm.9	|- F:NN-->X
xplm.10	|- G:NN-->Y
xplm.11	|- H = {<.k, w>. | (k e. NN /\ w = <.(F` k), (G` k)>.)}

Assertion

Ref	Expression
xplm	|- ((F(~~>m` B)R /\ G(~~>m` C)S) <-> H(~~>m` D)<.R, 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   k,F,w,x,y,z   k,G,w,x,y,z

Proof of Theorem xplm

Step	Hyp	Ref	Expression
1		opelxpi 3217	. . . . 5 |- ((R e. X /\ S e. Y) -> <.R, S>. e. (X X. Y))
2		xplm.5	. . . . . 6 |- B e. Met
3		xplm.a	. . . . . 6 |- R e. V
4		xplm.1	. . . . . . 7 |- X = dom dom B
5	4	lmcl 7949	. . . . . 6 |- ((B e. Met /\ R e. V /\ F(~~>m` B)R) -> R e. X)
6	2, 3, 5	mp3an12 906	. . . . 5 |- (F(~~>m` B)R -> R e. X)
7		xplm.6	. . . . . 6 |- C e. Met
8		xplm.b	. . . . . 6 |- S e. V
9		xplm.3	. . . . . . 7 |- Y = dom dom C
10	9	lmcl 7949	. . . . . 6 |- ((C e. Met /\ S e. V /\ G(~~>m` C)S) -> S e. Y)
11	7, 8, 10	mp3an12 906	. . . . 5 |- (G(~~>m` C)S -> S e. Y)
12	1, 6, 11	syl2an 454	. . . 4 |- ((F(~~>m` B)R /\ G(~~>m` C)S) -> <.R, S>. e. (X X. Y))
13		1z 6159	. . . . . . . . . . . . 13 |- 1 e. ZZ
14		nnuz 6439	. . . . . . . . . . . . 13 |- NN = (ZZ>` 1)
15	4, 13, 14	lmcvg2 7933	. . . . . . . . . . . 12 |- (((B e. Met /\ R e. V /\ F(~~>m` B)R) /\ (v e. RR /\ 0 < v)) -> E.n e. NN A.m e. NN (n <_ m -> ((F` m)BR) < v))
16	2, 15	mp3anl1 910	. . . . . . . . . . 11 |- (((R e. V /\ F(~~>m` B)R) /\ (v e. RR /\ 0 < v)) -> E.n e. NN A.m e. NN (n <_ m -> ((F` m)BR) < v))
17	3, 16	mpanl1 706	. . . . . . . . . 10 |- ((F(~~>m` B)R /\ (v e. RR /\ 0 < v)) -> E.n e. NN A.m e. NN (n <_ m -> ((F` m)BR) < v))
18	9, 13, 14	lmcvg2 7933	. . . . . . . . . . . 12 |- (((C e. Met /\ S e. V /\ G(~~>m` C)S) /\ (v e. RR /\ 0 < v)) -> E.p e. NN A.m e. NN (p <_ m -> ((G` m)CS) < v))
19	7, 18	mp3anl1 910	. . . . . . . . . . 11 |- (((S e. V /\ G(~~>m` C)S) /\ (v e. RR /\ 0 < v)) -> E.p e. NN A.m e. NN (p <_ m -> ((G` m)CS) < v))
20	8, 19	mpanl1 706	. . . . . . . . . 10 |- ((G(~~>m` C)S /\ (v e. RR /\ 0 < v)) -> E.p e. NN A.m e. NN (p <_ m -> ((G` m)CS) < v))
21	17, 20	anim12i 333	. . . . . . . . 9 |- (((F(~~>m` B)R /\ (v e. RR /\ 0 < v)) /\ (G(~~>m` C)S /\ (v e. RR /\ 0 < v))) -> (E.n e. NN A.m e. NN (n <_ m -> ((F` m)BR) < v) /\ E.p e. NN A.m e. NN (p <_ m -> ((G` m)CS) < v)))
22	21	anandirs 513	. . . . . . . 8 |- (((F(~~>m` B)R /\ G(~~>m` C)S) /\ (v e. RR /\ 0 < v)) -> (E.n e. NN A.m e. NN (n <_ m -> ((F` m)BR) < v) /\ E.p e. NN A.m e. NN (p <_ m -> ((G` m)CS) < v)))
23		reeanv 1778	. . . . . . . . 9 |- (E.n e. NN E.p e. NN (A.m e. NN (n <_ m -> ((F` m)BR) < v) /\ A.m e. NN (p <_ m -> ((G` m)CS) < v)) <-> (E.n e. NN A.m e. NN (n <_ m -> ((F` m)BR) < v) /\ E.p e. NN A.m e. NN (p <_ m -> ((G` m)CS) < v)))
24		nnret 5929	. . . . . . . . . . . . 13 |- (n e. NN -> n e. RR)
25	24	adantr 389	. . . . . . . . . . . 12 |- ((n e. NN /\ p e. NN) -> n e. RR)
26		nnret 5929	. . . . . . . . . . . . 13 |- (p e. NN -> p e. RR)
27	26	adantl 388	. . . . . . . . . . . 12 |- ((n e. NN /\ p e. NN) -> p e. RR)
28		letrt 5525	. . . . . . . . . . . . . . . . . . . . . 22 |- ((n e. RR /\ p e. RR /\ m e. RR) -> ((n <_ p /\ p <_ m) -> n <_ m))
29		nnret 5929	. . . . . . . . . . . . . . . . . . . . . 22 |- (m e. NN -> m e. RR)
30	28, 24, 26, 29	syl3an 868	. . . . . . . . . . . . . . . . . . . . 21 |- ((n e. NN /\ p e. NN /\ m e. NN) -> ((n <_ p /\ p <_ m) -> n <_ m))
31	30	3expa 833	. . . . . . . . . . . . . . . . . . . 20 |- (((n e. NN /\ p e. NN) /\ m e. NN) -> ((n <_ p /\ p <_ m) -> n <_ m))
32	31	exp3a 375	. . . . . . . . . . . . . . . . . . 19 |- (((n e. NN /\ p e. NN) /\ m e. NN) -> (n <_ p -> (p <_ m -> n <_ m)))
33	32	imp 350	. . . . . . . . . . . . . . . . . 18 |- ((((n e. NN /\ p e. NN) /\ m e. NN) /\ n <_ p) -> (p <_ m -> n <_ m))
34	33	an1rs 489	. . . . . . . . . . . . . . . . 17 |- ((((n e. NN /\ p e. NN) /\ n <_ p) /\ m e. NN) -> (p <_ m -> n <_ m))
35	34	ancrd 299	. . . . . . . . . . . . . . . 16 |- ((((n e. NN /\ p e. NN) /\ n <_ p) /\ m e. NN) -> (p <_ m -> (n <_ m /\ p <_ m)))
36	35	imim1d 28	. . . . . . . . . . . . . . 15 |- ((((n e. NN /\ p e. NN) /\ n <_ p) /\ m e. NN) -> (((n <_ m /\ p <_ m) -> (((F` m)BR) < v /\ ((G` m)CS) < v)) -> (p <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v))))
37	36	r19.20dva 1709	. . . . . . . . . . . . . 14 |- (((n e. NN /\ p e. NN) /\ n <_ p) -> (A.m e. NN ((n <_ m /\ p <_ m) -> (((F` m)BR) < v /\ ((G` m)CS) < v)) -> A.m e. NN (p <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v))))
38		simplr 413	. . . . . . . . . . . . . 14 |- (((n e. NN /\ p e. NN) /\ n <_ p) -> p e. NN)
39	37, 38	jctild 601	. . . . . . . . . . . . 13 |- (((n e. NN /\ p e. NN) /\ n <_ p) -> (A.m e. NN ((n <_ m /\ p <_ m) -> (((F` m)BR) < v /\ ((G` m)CS) < v)) -> (p e. NN /\ A.m e. NN (p <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v)))))
40		breq1 2622	. . . . . . . . . . . . . . . 16 |- (j = p -> (j <_ m <-> p <_ m))
41	40	imbi1d 613	. . . . . . . . . . . . . . 15 |- (j = p -> ((j <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v)) <-> (p <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v))))
42	41	ralbidv 1663	. . . . . . . . . . . . . 14 |- (j = p -> (A.m e. NN (j <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v)) <-> A.m e. NN (p <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v))))
43	42	rcla4ev 1877	. . . . . . . . . . . . 13 |- ((p e. NN /\ A.m e. NN (p <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v))) -> E.j e. NN A.m e. NN (j <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v)))
44	39, 43	syl6 22	. . . . . . . . . . . 12 |- (((n e. NN /\ p e. NN) /\ n <_ p) -> (A.m e. NN ((n <_ m /\ p <_ m) -> (((F` m)BR) < v /\ ((G` m)CS) < v)) -> E.j e. NN A.m e. NN (j <_ m -> (((F` m)BR) < v /\ ((G` m)CS) < v))))
45		letrt 5525	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((p e. RR /\ n e. RR /\ m e. RR) -> ((p <_ n /\ n <_ m) -> p <_ m))
46	45, 26, 24, 29	syl3an 868	. . . . . . . . . . . . . . . . . . . . . 22 |- ((p e. NN /\ n e. NN /\ m e. NN) -> ((p <_ n /\ n <_ m) -> p <_ m))
47	46	3com12 837	. . . . . . . . . . . . . . . . . . . . 21 |- ((n e. NN /\ p e. NN /\ m e. NN) -> ((p <_ n /\ n <_