Theorem metcn4i 7969

Description: Convergence carries through a continuous mapping.

Hypotheses

Ref	Expression
metcn4i.1	|- X = dom dom C
metcn4i.c	|- J = (Open` C)
metcn4i.d	|- K = (Open` D)
metcn4i.5	|- H = {<.j, y>. | (j e. NN /\ y = (F` (G` j)))}
metcn4i.p	|- P e. V

Assertion

Ref	Expression
metcn4i	|- (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ (G:NN-->X /\ G(~~>m` C)P)) -> H(~~>m` D)(F` P))

Distinct variable groups:   y,j,D   j,F,y   j,G,y   j,X

Proof of Theorem metcn4i

Step	Hyp	Ref	Expression
1		metcn4i.p	. . . . 5 |- P e. V
2		metcn4i.1	. . . . . 6 |- X = dom dom C
3	2	lmcl 7946	. . . . 5 |- ((C e. Met /\ P e. V /\ G(~~>m` C)P) -> P e. X)
4	1, 3	mp3an2 906	. . . 4 |- ((C e. Met /\ G(~~>m` C)P) -> P e. X)
5	4	ad2ant2rl 413	. . 3 |- (((C e. Met /\ F e. (J Cn K)) /\ (G:NN-->X /\ G(~~>m` C)P)) -> P e. X)
6	5	3adantl2 806	. 2 |- (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ (G:NN-->X /\ G(~~>m` C)P)) -> P e. X)
7		breq2 2628	. . . . . . . 8 |- (p = P -> (G(~~>m` C)p <-> G(~~>m` C)P))
8		fveq2 3730	. . . . . . . . 9 |- (p = P -> (F` p) = (F` P))
9	8	breq2d 2635	. . . . . . . 8 |- (p = P -> (H(~~>m` D)(F` p) <-> H(~~>m` D)(F` P)))
10	7, 9	imbi12d 628	. . . . . . 7 |- (p = P -> ((G(~~>m` C)p -> H(~~>m` D)(F` p)) <-> (G(~~>m` C)P -> H(~~>m` D)(F` P))))
11	10	rcla4v 1876	. . . . . 6 |- (P e. X -> (A.p e. X (G(~~>m` C)p -> H(~~>m` D)(F` p)) -> (G(~~>m` C)P -> H(~~>m` D)(F` P))))
12		nnex 5935	. . . . . . . . 9 |- NN e. V
13		fex 3658	. . . . . . . . 9 |- ((G:NN-->X /\ NN e. V) -> G e. V)
14	12, 13	mpan2 698	. . . . . . . 8 |- (G:NN-->X -> G e. V)
15		feq1 3626	. . . . . . . . . . . 12 |- (g = G -> (g:NN-->X <-> G:NN-->X))
16		breq1 2627	. . . . . . . . . . . . . 14 |- (g = G -> (g(~~>m` C)p <-> G(~~>m` C)p))
17		fveq1 3729	. . . . . . . . . . . . . . . . . . . 20 |- (g = G -> (g` j) = (G` j))
18	17	fveq2d 3734	. . . . . . . . . . . . . . . . . . 19 |- (g = G -> (F` (g` j)) = (F` (G` j)))
19	18	eqeq2d 1489	. . . . . . . . . . . . . . . . . 18 |- (g = G -> (y = (F` (g` j)) <-> y = (F` (G` j))))
20	19	anbi2d 618	. . . . . . . . . . . . . . . . 17 |- (g = G -> ((j e. NN /\ y = (F` (g` j))) <-> (j e. NN /\ y = (F` (G` j)))))
21	20	opabbidv 2675	. . . . . . . . . . . . . . . 16 |- (g = G -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} = {<.j, y>. | (j e. NN /\ y = (F` (G` j)))})
22		metcn4i.5	. . . . . . . . . . . . . . . 16 |- H = {<.j, y>. | (j e. NN /\ y = (F` (G` j)))}
23	21, 22	syl6eqr 1528	. . . . . . . . . . . . . . 15 |- (g = G -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} = H)
24	23	breq1d 2634	. . . . . . . . . . . . . 14 |- (g = G -> ({<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p) <-> H(~~>m` D)(F` p)))
25	16, 24	imbi12d 628	. . . . . . . . . . . . 13 |- (g = G -> ((g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p)) <-> (G(~~>m` C)p -> H(~~>m` D)(F` p))))
26	25	ralbidv 1666	. . . . . . . . . . . 12 |- (g = G -> (A.p e. X (g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p)) <-> A.p e. X (G(~~>m` C)p -> H(~~>m` D)(F` p))))
27	15, 26	imbi12d 628	. . . . . . . . . . 11 |- (g = G -> ((g:NN-->X -> A.p e. X (g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p))) <-> (G:NN-->X -> A.p e. X (G(~~>m` C)p -> H(~~>m` D)(F` p)))))
28	27	cla4gv 1865	. . . . . . . . . 10 |- (G e. V -> (A.g(g:NN-->X -> A.p e. X (g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p))) -> (G:NN-->X -> A.p e. X (G(~~>m` C)p -> H(~~>m` D)(F` p)))))
29		eqid 1478	. . . . . . . . . . . 12 |- dom dom D = dom dom D
30		metcn4i.c	. . . . . . . . . . . 12 |- J = (Open` C)
31		metcn4i.d	. . . . . . . . . . . 12 |- K = (Open` D)
32	2, 29, 30, 31	metcnf 7881	. . . . . . . . . . 11 |- ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> F:X-->dom dom D)
33		eqid 1478	. . . . . . . . . . . . . . . 16 |- {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} = {<.j, y>. | (j e. NN /\ y = (F` (g` j)))}
34	2, 29, 30, 31, 33	metcn4 7968	. . . . . . . . . . . . . . 15 |- ((C e. Met /\ D e. Met /\ F:X-->dom dom D) -> (F e. (J Cn K) <-> A.g(g:NN-->X -> A.p e. X (g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p)))))
35	34	biimpd 153	. . . . . . . . . . . . . 14 |- ((C e. Met /\ D e. Met /\ F:X-->dom dom D) -> (F e. (J Cn K) -> A.g(g:NN-->X -> A.p e. X (g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p)))))
36	35	3exp 834	. . . . . . . . . . . . 13 |- (C e. Met -> (D e. Met -> (F:X-->dom dom D -> (F e. (J Cn K) -> A.g(g:NN-->X -> A.p e. X (g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p)))))))
37	36	com34 36	. . . . . . . . . . . 12 |- (C e. Met -> (D e. Met -> (F e. (J Cn K) -> (F:X-->dom dom D -> A.g(g:NN-->X -> A.p e. X (g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p)))))))
38	37	3imp 829	. . . . . . . . . . 11 |- ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> (F:X-->dom dom D -> A.g(g:NN-->X -> A.p e. X (g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p)))))
39	32, 38	mpd 26	. . . . . . . . . 10 |- ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> A.g(g:NN-->X -> A.p e. X (g(~~>m` C)p -> {<.j, y>. | (j e. NN /\ y = (F` (g` j)))} (~~>m` D)(F` p))))
40	28, 39	syl5 21	. . . . . . . . 9 |- (G e. V -> ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> (G:NN-->X -> A.p e. X (G(~~>m` C)p -> H(~~>m` D)(F` p)))))
41	40	com3l 34	. . . . . . . 8 |- ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> (G:NN-->X -> (G e. V -> A.p e. X (G(~~>m` C)p -> H(~~>m` D)(F` p)))))
42	14, 41	mpdi 48	. . . . . . 7 |- ((C e. Met /\ D e. Met /\ F e. (J Cn K)) -> (G:NN-->X -> A.p e. X (G(~~>m` C)p -> H(~~>m` D)(F` p))))
43	42	imp 350	. . . . . 6 |- (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ G:NN-->X) -> A.p e. X (G(~~>m` C)p -> H(~~>m` D)(F` p)))
44	11, 43	syl5 21	. . . . 5 |- (P e. X -> (((C e. Met /\ D e. Met /\ F e. (J Cn K)) /\ G:NN-->X) -> (G(~~>m` C)P -> H(~~>m` D)(F` P))))
45	44	com3l 34	. . . 4 |- (((C e. Met /\ D e. Met /\ F e. (J Cn K