Theorem xplmi 7973

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 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, < ))}
xplmi.9	|- F = {<.k, w>. | (k e. NN /\ w = (1st` (H` k)))}
xplmi.10	|- G = {<.k, w>. | (k e. NN /\ w = (2nd` (H` k)))}

Assertion

Ref	Expression
xplmi	|- ((H:NN-->(X X. Y) /\ H(~~>m` D)<.R, S>.) -> ((F:NN-->X /\ F(~~>m` B)R) /\ (G:NN-->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 414	. . . . . . . 8 |- ((H(~~>m` D)<.R, S>. /\ (R e. X /\ S e. Y)) -> R e. X)
2	1	a1i 8	. . . . . . 7 |- (H:NN-->(X X. Y) -> ((H(~~>m` D)<.R, S>. /\ (R e. X /\ S e. Y)) -> R e. X))
3		opex 2782	. . . . . . . . . . . . 13 |- <.R, S>. e. V
4		xplm.1	. . . . . . . . . . . . . . 15 |- X = dom dom B
5		xplm.3	. . . . . . . . . . . . . . 15 |- Y = dom dom C
6		xplm.5	. . . . . . . . . . . . . . 15 |- B e. Met
7		xplm.6	. . . . . . . . . . . . . . 15 |- C e. Met
8		xplm.7	. . . . . . . . . . . . . . 15 |- 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, < ))}
9	4, 5, 6, 7, 8	metxp 7834	. . . . . . . . . . . . . 14 |- D e. Met
10		ltso 5512	. . . . . . . . . . . . . . . . . . 19 |- < Or RR
11	10	supex 4577	. . . . . . . . . . . . . . . . . 18 |- sup({((1st` x)B(1st` y)), ((2nd` x)C(2nd` y))}, RR, < ) e. V
12	11, 8	dmoprab2 4123	. . . . . . . . . . . . . . . . 17 |- dom D = ((X X. Y) X. (X X. Y))
13	12	dmeqi 3312	. . . . . . . . . . . . . . . 16 |- dom dom D = dom ((X X. Y) X. (X X. Y))
14		dmxpid 3333	. . . . . . . . . . . . . . . 16 |- dom ((X X. Y) X. (X X. Y)) = (X X. Y)
15	13, 14	eqtr2 1496	. . . . . . . . . . . . . . 15 |- (X X. Y) = dom dom D
16		1z 6159	. . . . . . . . . . . . . . 15 |- 1 e. ZZ
17		nnuz 6439	. . . . . . . . . . . . . . 15 |- NN = (ZZ>` 1)
18	15, 16, 17	lmcvg2 7933	. . . . . . . . . . . . . 14 |- (((D e. Met /\ <.R, S>. e. V /\ H(~~>m` D)<.R, S>.) /\ (v e. RR /\ 0 < v)) -> E.j e. NN A.m e. NN (j <_ m -> ((H` m)D<.R, S>.) < v))
19	9, 18	mp3anl1 910	. . . . . . . . . . . . 13 |- (((<.R, S>. e. V /\ H(~~>m` D)<.R, S>.) /\ (v e. RR /\ 0 < v)) -> E.j e. NN A.m e. NN (j <_ m -> ((H` m)D<.R, S>.) < v))
20	3, 19	mpanl1 706	. . . . . . . . . . . 12 |- ((H(~~>m` D)<.R, S>. /\ (v e. RR /\ 0 < v)) -> E.j e. NN A.m e. NN (j <_ m -> ((H` m)D<.R, S>.) < v))
21	20	adantlr 393	. . . . . . . . . . 11 |- (((H(~~>m` D)<.R, S>. /\ (R e. X /\ S e. Y)) /\ (v e. RR /\ 0 < v)) -> E.j e. NN A.m e. NN (j <_ m -> ((H` m)D<.R, S>.) < v))
22	21	adantll 392	. . . . . . . . . 10 |- (((H:NN-->(X X. Y) /\ (H(~~>m` D)<.R, S>. /\ (R e. X /\ S e. Y))) /\ (v e. RR /\ 0 < v)) -> E.j e. NN A.m e. NN (j <_ m -> ((H` m)D<.R, S>.) < v))
23		ffvelrn 3814	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((H:NN-->(X X. Y) /\ m e. NN) -> (H` m) e. (X X. Y))
24		elxp6 4102	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((H` m) e. (X X. Y) <-> ((H` m) = <.(1st` (H` m)), (2nd` (H` m))>. /\ ((1st` (H` m)) e. X /\ (2nd` (H` m)) e. Y)))
25	24	pm3.26bi 322	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((H` m) e. (X X. Y) -> (H` m) = <.(1st` (H` m)), (2nd` (H` m))>.)
26	23, 25	syl 10	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((H:NN-->(X X. Y) /\ m e. NN) -> (H` m) = <.(1st` (H` m)), (2nd` (H` m))>.)
27		fveq2 3724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (k = m -> (H` k) = (H` m))
28	27	fveq2d 3728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (k = m -> (1st` (H` k)) = (1st` (H` m)))
29		xplmi.9	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- F = {<.k, w>. | (k e. NN /\ w = (1st` (H` k)))}
30		fvex 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (1st` (H` m)) e. V
31	28, 29, 30	fvopab4 3780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (m e. NN -> (F` m) = (1st` (H` m)))
32	27	fveq2d 3728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (k = m -> (2nd` (H` k)) = (2nd` (H` m)))
33		xplmi.10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- G = {<.k, w>. | (k e. NN /\ w = (2nd` (H` k)))}
34		fvex 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (2nd` (H` m)) e. V
35	32, 33, 34	fvopab4 3780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (m e. NN -> (G` m) = (2nd` (H` m)))
36	31, 35	opeq12d 2495	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (m e. NN -> <.(F` m), (G` m)>. = <.(1st` (H` m)), (2nd` (H` m))>.)
37	36	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((H:NN-->(X X. Y) /\ m e. NN) -> <.(F` m), (G` m)>. = <.(1st` (H` m)), (2nd` (H` m))>.)
38	26, 37	eqtr4d 1510	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((H:NN-->(X X. Y) /\ m e. NN) -> (H` m) = <.(F` m), (G` m)>.)
39	38	opreq1d 3975	. . . . . . . . . . . . . . . . . . . . . 22 |- ((H:NN-->(X X. Y) /\ m e. NN) -> ((H` m)D<.R, S>.) = (<.(F` m), (G` m)>.D<.R, S>.))
40	39	breq1d 2629	. . . . . . . . . . . . . . . . . . . . 21 |- ((H:NN-->(X X. Y) /\ m e. NN) -> (((H` m)D<.R, S>.) < v <-> (<.(F` m), (G` m)>.D<.R, S>.) < v))
41	40	adantr 389	. . . . . . . . . . . . . . . . . . . 20 |- (((H:NN-->(X X. Y) /\ m e. NN) /\ ((R e. X /\ S e. Y) /\ v e. RR)) -> (((H` m)D<.R, S>.) < v <-> (<.(F` m), (G` m)>.D<.R, S>.) < v))
42	5	metcl 7811	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((C e. Met /\ (G` m) e. Y /\ S e. Y) -> ((G` m)CS) e. RR)
43	7, 42	mp3an1 903	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((G` m) e. Y /\ S e. Y) -> ((G` m)CS) e. RR)
44		ffvelrn 3814	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((G:NN-->Y /\ m e. NN) -> (G` m) e. Y)
45		ffvelrn 3814	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((H:NN-->(X X. Y) /\ k e. NN) -> (H` k) e. (X X. Y))
46		elxp7 4103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((H` k) e. (X X. Y) <-> ((H` k) e. (V X. V) /\ ((1st` (H` k)) e. X /\ (2nd` (H` k)) e. Y)))
47	46	pm3.27bi 326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((H` k) e. (X X. Y) -> ((1st` (H` k)) e. X /\ (2nd` (H` k)) e. Y))
48	47	pm3.27d 325	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((H` k) e. (X X. Y) -> (2nd` (H` k)) e. Y)
49	45, 48	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((H:NN-->(X X. Y) /\ k e. NN) -> (2nd` (H` k)) e. Y)
50	49	r19.21aiva 1714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (H:NN-->(X X. Y) -> A.k e. NN (2nd` (H` k)) e. Y)
51	33	fopab2 3823	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (A.k e. NN (2nd` (H` k)) e. Y <-> G:NN-->Y)
52	50, 51	sylib 198	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (H:NN-->(X X. Y) -> G:NN-->Y)
53	44, 52	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((H:NN-->(X X. Y) /\ m e. NN) -> (G` m) e. Y)
54	43, 53	sylan 448	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((H:NN-->(X X. Y) /\ m e. NN) /\ S e. Y) -> ((G` m)CS) e. RR)
55	54	adantrl 394	. . . . . . . . . . . . . . . . . . . . . 22 |- (((H: