lmcn2

Description: The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 15-May-2014)

	Ref	Expression
Hypotheses	txlm.z	\|- Z = ( ZZ>= ` M )
	txlm.m	\|- ( ph -> M e. ZZ )
	txlm.j	\|- ( ph -> J e. ( TopOn ` X ) )
	txlm.k	\|- ( ph -> K e. ( TopOn ` Y ) )
	txlm.f	\|- ( ph -> F : Z --> X )
	txlm.g	\|- ( ph -> G : Z --> Y )
	lmcn2.fl	\|- ( ph -> F ( ~~>t ` J ) R )
	lmcn2.gl	\|- ( ph -> G ( ~~>t ` K ) S )
	lmcn2.o	\|- ( ph -> O e. ( ( J tX K ) Cn N ) )
	lmcn2.h	\|- H = ( n e. Z \|-> ( ( F ` n ) O ( G ` n ) ) )
Assertion	lmcn2	\|- ( ph -> H ( ~~>t ` N ) ( R O S ) )

Proof

Step	Hyp	Ref	Expression
1		txlm.z	\|- Z = ( ZZ>= ` M )
2		txlm.m	\|- ( ph -> M e. ZZ )
3		txlm.j	\|- ( ph -> J e. ( TopOn ` X ) )
4		txlm.k	\|- ( ph -> K e. ( TopOn ` Y ) )
5		txlm.f	\|- ( ph -> F : Z --> X )
6		txlm.g	\|- ( ph -> G : Z --> Y )
7		lmcn2.fl	\|- ( ph -> F ( ~~>t ` J ) R )
8		lmcn2.gl	\|- ( ph -> G ( ~~>t ` K ) S )
9		lmcn2.o	\|- ( ph -> O e. ( ( J tX K ) Cn N ) )
10		lmcn2.h	\|- H = ( n e. Z \|-> ( ( F ` n ) O ( G ` n ) ) )
11	5	ffvelrnda	\|- ( ( ph /\ n e. Z ) -> ( F ` n ) e. X )
12	6	ffvelrnda	\|- ( ( ph /\ n e. Z ) -> ( G ` n ) e. Y )
13	11 12	opelxpd	\|- ( ( ph /\ n e. Z ) -> <. ( F ` n ) , ( G ` n ) >. e. ( X X. Y ) )
14		eqidd	\|- ( ph -> ( n e. Z \|-> <. ( F ` n ) , ( G ` n ) >. ) = ( n e. Z \|-> <. ( F ` n ) , ( G ` n ) >. ) )
15		txtopon	\|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
16	3 4 15	syl2anc	\|- ( ph -> ( J tX K ) e. ( TopOn ` ( X X. Y ) ) )
17		cntop2	\|- ( O e. ( ( J tX K ) Cn N ) -> N e. Top )
18	9 17	syl	\|- ( ph -> N e. Top )
19		toptopon2	\|- ( N e. Top <-> N e. ( TopOn ` U. N ) )
20	18 19	sylib	\|- ( ph -> N e. ( TopOn ` U. N ) )
21		cnf2	\|- ( ( ( J tX K ) e. ( TopOn ` ( X X. Y ) ) /\ N e. ( TopOn ` U. N ) /\ O e. ( ( J tX K ) Cn N ) ) -> O : ( X X. Y ) --> U. N )
22	16 20 9 21	syl3anc	\|- ( ph -> O : ( X X. Y ) --> U. N )
23	22	feqmptd	\|- ( ph -> O = ( x e. ( X X. Y ) \|-> ( O ` x ) ) )
24		fveq2	\|- ( x = <. ( F ` n ) , ( G ` n ) >. -> ( O ` x ) = ( O ` <. ( F ` n ) , ( G ` n ) >. ) )
25		df-ov	\|- ( ( F ` n ) O ( G ` n ) ) = ( O ` <. ( F ` n ) , ( G ` n ) >. )
26	24 25	eqtr4di	\|- ( x = <. ( F ` n ) , ( G ` n ) >. -> ( O ` x ) = ( ( F ` n ) O ( G ` n ) ) )
27	13 14 23 26	fmptco	\|- ( ph -> ( O o. ( n e. Z \|-> <. ( F ` n ) , ( G ` n ) >. ) ) = ( n e. Z \|-> ( ( F ` n ) O ( G ` n ) ) ) )
28	27 10	eqtr4di	\|- ( ph -> ( O o. ( n e. Z \|-> <. ( F ` n ) , ( G ` n ) >. ) ) = H )
29		eqid	\|- ( n e. Z \|-> <. ( F ` n ) , ( G ` n ) >. ) = ( n e. Z \|-> <. ( F ` n ) , ( G ` n ) >. )
30	1 2 3 4 5 6 29	txlm	\|- ( ph -> ( ( F ( ~~>t ` J ) R /\ G ( ~~>t ` K ) S ) <-> ( n e. Z \|-> <. ( F ` n ) , ( G ` n ) >. ) ( ~~>t ` ( J tX K ) ) <. R , S >. ) )
31	7 8 30	mpbi2and	\|- ( ph -> ( n e. Z \|-> <. ( F ` n ) , ( G ` n ) >. ) ( ~~>t ` ( J tX K ) ) <. R , S >. )
32	31 9	lmcn	\|- ( ph -> ( O o. ( n e. Z \|-> <. ( F ` n ) , ( G ` n ) >. ) ) ( ~~>t ` N ) ( O ` <. R , S >. ) )
33	28 32	eqbrtrrd	\|- ( ph -> H ( ~~>t ` N ) ( O ` <. R , S >. ) )
34		df-ov	\|- ( R O S ) = ( O ` <. R , S >. )
35	33 34	breqtrrdi	\|- ( ph -> H ( ~~>t ` N ) ( R O S ) )

Metamath Proof Explorer

Theorem lmcn2

Proof