Theorem lmss 7953

Description: Limit on a metric subspace.

Assertion

Ref	Expression
lmss	|- ((D e. Met /\ P e. Y /\ F:NN-->Y) -> (F(~~>m` D)P <-> F(~~>m` (D |` (Y X. Y)))P))

Proof of Theorem lmss

Step	Hyp	Ref	Expression
1		eqid 1475	. . . . . 6 |- dom dom D = dom dom D
2	1	lmfss 7948	. . . . 5 |- ((D e. Met /\ P e. Y /\ F(~~>m` D)P) -> F (_ (CC X. dom dom D))
3	2	3expa 833	. . . 4 |- (((D e. Met /\ P e. Y) /\ F(~~>m` D)P) -> F (_ (CC X. dom dom D))
4	3	adantlrr 399	. . 3 |- (((D e. Met /\ (P e. Y /\ F:NN-->Y)) /\ F(~~>m` D)P) -> F (_ (CC X. dom dom D))
5		eqid 1475	. . . . . 6 |- dom dom ( D |` (Y X. Y)) = dom dom ( D |` (Y X. Y))
6	5	lmfss 7948	. . . . 5 |- (((D |` (Y X. Y)) e. Met /\ P e. Y /\ F(~~>m` (D |` (Y X. Y)))P) -> F (_ (CC X. dom dom ( D |` (Y X. Y))))
7	6	3expa 833	. . . 4 |- ((((D |` (Y X. Y)) e. Met /\ P e. Y) /\ F(~~>m` (D |` (Y X. Y)))P) -> F (_ (CC X. dom dom ( D |` (Y X. Y))))
8	7	adantlrr 399	. . 3 |- ((((D |` (Y X. Y)) e. Met /\ (P e. Y /\ F:NN-->Y)) /\ F(~~>m` (D |` (Y X. Y)))P) -> F (_ (CC X. dom dom ( D |` (Y X. Y))))
9	1	metssba 7809	. . . . . . . . . 10 |- (D e. Met -> (dom dom D i^i Y) = dom dom ( D |` (Y X. Y)))
10		incom 2208	. . . . . . . . . 10 |- (Y i^i dom dom D) = (dom dom D i^i Y)
11	9, 10	syl5req 1520	. . . . . . . . 9 |- (D e. Met -> dom dom ( D |` (Y X. Y)) = (Y i^i dom dom D))
12	11	eleq2d 1541	. . . . . . . 8 |- (D e. Met -> (P e. dom dom ( D |` (Y X. Y)) <-> P e. (Y i^i dom dom D)))
13		elin 2207	. . . . . . . . 9 |- (P e. (Y i^i dom dom D) <-> (P e. Y /\ P e. dom dom D))
14	13	baib 685	. . . . . . . 8 |- (P e. Y -> (P e. (Y i^i dom dom D) <-> P e. dom dom D))
15	12, 14	sylan9bb 540	. . . . . . 7 |- ((D e. Met /\ P e. Y) -> (P e. dom dom ( D |` (Y X. Y)) <-> P e. dom dom D))
16	15	adantrr 395	. . . . . 6 |- ((D e. Met /\ (P e. Y /\ F:NN-->Y)) -> (P e. dom dom ( D |` (Y X. Y)) <-> P e. dom dom D))
17		oprvalres 4033	. . . . . . . . . . . . . . . 16 |- (((F` k) e. Y /\ P e. Y) -> ((F` k)(D |` (Y X. Y))P) = ((F` k)DP))
18		ffvelrn 3814	. . . . . . . . . . . . . . . 16 |- ((F:NN-->Y /\ k e. NN) -> (F` k) e. Y)
19	17, 18	sylan 448	. . . . . . . . . . . . . . 15 |- (((F:NN-->Y /\ k e. NN) /\ P e. Y) -> ((F` k)(D |` (Y X. Y))P) = ((F` k)DP))
20	19	ancoms 436	. . . . . . . . . . . . . 14 |- ((P e. Y /\ (F:NN-->Y /\ k e. NN)) -> ((F` k)(D |` (Y X. Y))P) = ((F` k)DP))
21	20	anassrs 441	. . . . . . . . . . . . 13 |- (((P e. Y /\ F:NN-->Y) /\ k e. NN) -> ((F` k)(D |` (Y X. Y))P) = ((F` k)DP))
22	21	breq1d 2629	. . . . . . . . . . . 12 |- (((P e. Y /\ F:NN-->Y) /\ k e. NN) -> (((F` k)(D |` (Y X. Y))P) < x <-> ((F` k)DP) < x))
23	22	imbi2d 612	. . . . . . . . . . 11 |- (((P e. Y /\ F:NN-->Y) /\ k e. NN) -> ((j <_ k -> ((F` k)(D |` (Y X. Y))P) < x) <-> (j <_ k -> ((F` k)DP) < x)))
24	23	ralbidva 1659	. . . . . . . . . 10 |- ((P e. Y /\ F:NN-->Y) -> (A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x) <-> A.k e. NN (j <_ k -> ((F` k)DP) < x)))
25	24	rexbidv 1664	. . . . . . . . 9 |- ((P e. Y /\ F:NN-->Y) -> (E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x) <-> E.j e. NN A.k e. NN (j <_ k -> ((F` k)DP) < x)))
26	25	imbi2d 612	. . . . . . . 8 |- ((P e. Y /\ F:NN-->Y) -> ((0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x)) <-> (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)DP) < x))))
27	26	ralbidv 1663	. . . . . . 7 |- ((P e. Y /\ F:NN-->Y) -> (A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x)) <-> A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)DP) < x))))
28	27	adantl 388	. . . . . 6 |- ((D e. Met /\ (P e. Y /\ F:NN-->Y)) -> (A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x)) <-> A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)DP) < x))))
29	16, 28	anbi12d 628	. . . . 5 |- ((D e. Met /\ (P e. Y /\ F:NN-->Y)) -> ((P e. dom dom ( D |` (Y X. Y)) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x))) <-> (P e. dom dom D /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)DP) < x)))))
30	29	adantrr 395	. . . 4 |- ((D e. Met /\ ((P e. Y /\ F:NN-->Y) /\ F:NN-->dom dom ( D |` (Y X. Y)))) -> ((P e. dom dom ( D |` (Y X. Y)) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x))) <-> (P e. dom dom D /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)DP) < x)))))
31		1z 6159	. . . . . . . 8 |- 1 e. ZZ
32		nnuz 6439	. . . . . . . 8 |- NN = (ZZ>` 1)
33	5, 31, 32	lmbrf 7930	. . . . . . 7 |- (((D |` (Y X. Y)) e. Met /\ P e. Y /\ F:NN-->dom dom ( D |` (Y X. Y))) -> (F(~~>m` (D |` (Y X. Y)))P <-> (P e. dom dom ( D |` (Y X. Y)) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x)))))
34		metres 7823	. . . . . . 7 |- (D e. Met -> (D |` (Y X. Y)) e. Met)
35	33, 34	syl3an1 859	. . . . . 6 |- ((D e. Met /\ P e. Y /\ F:NN-->dom dom ( D |` (Y X. Y))) -> (F(~~>m` (D |` (Y X. Y)))P <-> (P e. dom dom ( D |` (Y X. Y)) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x)))))
36	35	3expb 834	. . . . 5 |- ((D e. Met /\ (P e. Y /\ F:NN-->dom dom ( D |` (Y X. Y)))) -> (F(~~>m` (D |` (Y X. Y)))P <-> (P e. dom dom ( D |` (Y X. Y)) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x)))))
37	36	adantrlr 401	. . . 4 |- ((D e. Met /\ ((P e. Y /\ F:NN-->Y) /\ F:NN-->dom dom ( D |` (Y X. Y)))) -> (F(~~>m` (D |` (Y X. Y)))P <-> (P e. dom dom ( D |` (Y X. Y)) /\ A.x e. RR (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` k)(D |` (Y X. Y))P) < x)))))
38	1, 31, 32	lmbrf 7930	. . . . . . 7 |- ((D e. Met /\ P e. Y /\ F:NN-->dom dom D) -> (F(~~>m` D)