Theorem tlmval 16727

Description: The convergence relation on sequences in a topological space.

Hypothesis

Ref	Expression
tlmval.1	|- X = U.J

Assertion

Ref	Expression
tlmval	|- (J e. Top -> (~~>t` J) = {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)})

Distinct variable groups:   f,J,x,u,m,n   f,X,x,u,m,n

Proof of Theorem tlmval

Step	Hyp	Ref	Expression
1		fssxp 4669	. . . . . . . . 9 |- (f:NN-->X -> f C_ (NN X. X))
2		visset 2541	. . . . . . . . . 10 |- f e. _V
3	2	elpw 3231	. . . . . . . . 9 |- (f e. ~P(NN X. X) <-> f C_ (NN X. X))
4	1, 3	sylibr 243	. . . . . . . 8 |- (f:NN-->X -> f e. ~P(NN X. X))
5	4	anim1i 538	. . . . . . 7 |- ((f:NN-->X /\ x e. X) -> (f e. ~P(NN X. X) /\ x e. X))
6	5	anim1i 538	. . . . . 6 |- (((f:NN-->X /\ x e. X) /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u) -> ((f e. ~P(NN X. X) /\ x e. X) /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u))
7	6	3impa 1312	. . . . 5 |- ((f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u) -> ((f e. ~P(NN X. X) /\ x e. X) /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u))
8	7	ssopab2i 3735	. . . 4 |- {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)} C_ {<.f, x>. | ((f e. ~P(NN X. X) /\ x e. X) /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)}
9		opabssxp 4193	. . . 4 |- {<.f, x>. | ((f e. ~P(NN X. X) /\ x e. X) /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)} C_ (~P(NN X. X) X. X)
10	8, 9	sstri 2856	. . 3 |- {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)} C_ (~P(NN X. X) X. X)
11		nnex 7449	. . . . . 6 |- NN e. _V
12		tlmval.1	. . . . . . 7 |- X = U.J
13		uniexg 3934	. . . . . . 7 |- (J e. Top -> U.J e. _V)
14	12, 13	syl5eqel 2222	. . . . . 6 |- (J e. Top -> X e. _V)
15		xpexg 4225	. . . . . 6 |- ((NN e. _V /\ X e. _V) -> (NN X. X) e. _V)
16	11, 14, 15	sylancr 662	. . . . 5 |- (J e. Top -> (NN X. X) e. _V)
17		pwexg 3655	. . . . 5 |- ((NN X. X) e. _V -> ~P(NN X. X) e. _V)
18	16, 17	syl 13	. . . 4 |- (J e. Top -> ~P(NN X. X) e. _V)
19		xpexg 4225	. . . 4 |- ((~P(NN X. X) e. _V /\ X e. _V) -> (~P(NN X. X) X. X) e. _V)
20	18, 14, 19	syl11anc 659	. . 3 |- (J e. Top -> (~P(NN X. X) X. X) e. _V)
21		ssexg 3624	. . 3 |- (({<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)} C_ (~P(NN X. X) X. X) /\ (~P(NN X. X) X. X) e. _V) -> {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)} e. _V)
22	10, 20, 21	sylancr 662	. 2 |- (J e. Top -> {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)} e. _V)
23		unieq 3375	. . . . . . 7 |- (j = J -> U.j = U.J)
24	23, 12	syl6eqr 2195	. . . . . 6 |- (j = J -> U.j = X)
25		feq3 4649	. . . . . 6 |- (U.j = X -> (f:NN-->U.j <-> f:NN-->X))
26	24, 25	syl 13	. . . . 5 |- (j = J -> (f:NN-->U.j <-> f:NN-->X))
27	24	eleq2d 2211	. . . . 5 |- (j = J -> (x e. U.j <-> x e. X))
28		fveq2 4765	. . . . . . 7 |- (j = J -> (nei` j) = (nei` J))
29	28	fveq1d 4767	. . . . . 6 |- (j = J -> ((nei` j)` {x}) = ((nei` J)` {x}))
30	29	raleqdv 2515	. . . . 5 |- (j = J -> (A.u e. ((nei` j)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u <-> A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u))
31	26, 27, 30	3anbi123d 1441	. . . 4 |- (j = J -> ((f:NN-->U.j /\ x e. U.j /\ A.u e. ((nei` j)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u) <-> (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)))
32	31	opabbidv 3569	. . 3 |- (j = J -> {<.f, x>. | (f:NN-->U.j /\ x e. U.j /\ A.u e. ((nei` j)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)} = {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)})
33		df-tlm 16726	. . 3 |- ~~>t = {<.j, r>. | (j e. Top /\ r = {<.f, x>. | (f:NN-->U.j /\ x e. U.j /\ A.u e. ((nei` j)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)})}
34	32, 33	fvopab4g 4828	. 2 |- ((J e. Top /\ {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)} e. _V) -> (~~>t` J) = {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)})
35	22, 34	mpdan 673	1 |- (J e. Top -> (~~>t` J) = {<.f, x>. | (f:NN-->X /\ x e. X /\ A.u e. ((nei` J)` {x})E.n e. NN A.m e. (ZZ>=` n)(f` m) e. u)})

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588  A.wral 2355  E.wrex 2356  _Vcvv 2538   C_ wss 2827  ~Pcpw 3227  {csn 3238  U.cuni 3366  {copab 3565   X. cxp 4117  -->wf 4127  ` cfv 4131  NNcn 6992  ZZ>=cuz 7933  Topctop 9686  neicnei 9853  ~~>tctlm 16725

This theorem is referenced by:  tlmbr 16728

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-n 7441  df-tlm 16726

Copyright terms: Public domain