Theorem lmfval 10219

Description: The relation "sequence f converges to point y " in a metric space.

Hypothesis

Ref	Expression
lmfval.1	|- X = dom dom D

Assertion

Ref	Expression
lmfval	|- (D e. Met -> (~~>m` D) = {<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))})

Distinct variable groups:   f,j,k,x,y,D   f,X,y

Proof of Theorem lmfval

Step	Hyp	Ref	Expression
1		df-3an 1132	. . . . . 6 |- ((f e. ~P(CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))) <-> ((f e. ~P(CC X. X) /\ y e. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
2		visset 2572	. . . . . . . 8 |- f e. _V
3	2	elpw 3263	. . . . . . 7 |- (f e. ~P(CC X. X) <-> f C_ (CC X. X))
4	3	3anbi1i 1336	. . . . . 6 |- ((f e. ~P(CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))) <-> (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
5	1, 4	bitr3i 309	. . . . 5 |- (((f e. ~P(CC X. X) /\ y e. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))) <-> (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
6	5	opabbii 3602	. . . 4 |- {<.f, y>. | ((f e. ~P(CC X. X) /\ y e. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} = {<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))}
7		opabssxp 4225	. . . 4 |- {<.f, y>. | ((f e. ~P(CC X. X) /\ y e. X) /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} C_ (~P(CC X. X) X. X)
8	6, 7	eqsstr3i 2907	. . 3 |- {<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} C_ (~P(CC X. X) X. X)
9		lmfval.1	. . . . . 6 |- X = dom dom D
10		dmexg 4360	. . . . . . 7 |- (D e. Met -> dom D e. _V)
11		dmexg 4360	. . . . . . 7 |- (dom D e. _V -> dom dom D e. _V)
12	10, 11	syl 13	. . . . . 6 |- (D e. Met -> dom dom D e. _V)
13	9, 12	syl5eqel 2251	. . . . 5 |- (D e. Met -> X e. _V)
14		ax-cnex 6885	. . . . . 6 |- CC e. _V
15		xpexg 4257	. . . . . 6 |- ((CC e. _V /\ X e. _V) -> (CC X. X) e. _V)
16	14, 15	mpan 773	. . . . 5 |- (X e. _V -> (CC X. X) e. _V)
17		pwexg 3687	. . . . 5 |- ((CC X. X) e. _V -> ~P(CC X. X) e. _V)
18	13, 16, 17	3syl 38	. . . 4 |- (D e. Met -> ~P(CC X. X) e. _V)
19		xpexg 4257	. . . 4 |- ((~P(CC X. X) e. _V /\ X e. _V) -> (~P(CC X. X) X. X) e. _V)
20	18, 13, 19	syl11anc 755	. . 3 |- (D e. Met -> (~P(CC X. X) X. X) e. _V)
21		ssexg 3656	. . 3 |- (({<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} C_ (~P(CC X. X) X. X) /\ (~P(CC X. X) X. X) e. _V) -> {<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} e. _V)
22	8, 20, 21	sylancr 758	. 2 |- (D e. Met -> {<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} e. _V)
23		dmeq 4315	. . . . . . . . 9 |- (z = D -> dom z = dom D)
24	23	dmeqd 4317	. . . . . . . 8 |- (z = D -> dom dom z = dom dom D)
25	24, 9	syl6eqr 2224	. . . . . . 7 |- (z = D -> dom dom z = X)
26		xpeq2 4182	. . . . . . 7 |- (dom dom z = X -> (CC X. dom dom z) = (CC X. X))
27	25, 26	syl 13	. . . . . 6 |- (z = D -> (CC X. dom dom z) = (CC X. X))
28	27	sseq2d 2904	. . . . 5 |- (z = D -> (f C_ (CC X. dom dom z) <-> f C_ (CC X. X)))
29	25	eleq2d 2240	. . . . 5 |- (z = D -> (y e. dom dom z <-> y e. X))
30	25	eleq2d 2240	. . . . . . . . . 10 |- (z = D -> ((f` k) e. dom dom z <-> (f` k) e. X))
31	30	anbi1d 815	. . . . . . . . 9 |- (z = D -> (((f` k) e. dom dom z /\ ((f` k)Dy) < x) <-> ((f` k) e. X /\ ((f` k)Dy) < x)))
32	31	imbi2d 380	. . . . . . . 8 |- (z = D -> ((j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x)) <-> (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))
33	32	rexralbidv 2422	. . . . . . 7 |- (z = D -> (E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x)) <-> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))
34	33	imbi2d 380	. . . . . 6 |- (z = D -> ((0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))) <-> (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
35	34	ralbidv 2403	. . . . 5 |- (z = D -> (A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))) <-> A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x)))))
36	28, 29, 35	3anbi123d 1469	. . . 4 |- (z = D -> ((f C_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x)))) <-> (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))))
37	36	opabbidv 3601	. . 3 |- (z = D -> {<.f, y>. | (f C_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))} = {<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))})
38		df-lm 10216	. . 3 |- ~~>m = {<.z, w>. | (z e. Met /\ w = {<.f, y>. | (f C_ (CC X. dom dom z) /\ y e. dom dom z /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. dom dom z /\ ((f` k)Dy) < x))))})}
39	37, 38	fvopab4g 4867	. 2 |- ((D e. Met /\ {<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))} e. _V) -> (~~>m` D) = {<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))})
40	22, 39	mpdan 769	1 |- (D e. Met -> (~~>m` D) = {<.f, y>. | (f C_ (CC X. X) /\ y e. X /\ A.x e. RR (0 < x -> E.j e. ZZ A.k e. ZZ (j <_ k -> ((f` k) e. X /\ ((f` k)Dy) < x))))})

Syntax hints:   -> wi 3   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617  A.wral 2385  E.wrex 2386  _Vcvv 2569   C_ wss 2859  ~Pcpw 3259   class class class wbr 3539  {copab 3597   X. cxp 4149  dom cdm 4151  ` cfv 4163  (class class class)co 5020  CCcc 6827  RRcr 6828  0cc0 6829   <_ cle 6943   < clt 6947  ZZcz 7096  Metcme 10082  ~~>mclm 10213

This theorem is referenced by:  lmrel 10221  lmbr 10222  h2hlm 11478

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-cnex 6885

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-id 3779  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fv 4179  df-lm 10216

Copyright terms: Public domain