Theorem sfvlim 10596

Description: Functions whose values are the limits of the filters.

Hypothesis

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

Assertion

Ref	Expression
sfvlim	|- (J e. Top -> (fLim1` J) = {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})})

Distinct variable groups:   J,a,b,l   X,a,b,l

Proof of Theorem sfvlim

Step	Hyp	Ref	Expression
1		ssexg 2734	. . 3 |- (({<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})} (_ {<.a, b>. | (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})} /\ {<.a, b>. | (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})} e. V) -> {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})} e. V)
2		simpll 414	. . . . . . . . . . . 12 |- (((a e. Fil /\ U.a = X) /\ J e. Top) -> a e. Fil)
3		eqimss 2118	. . . . . . . . . . . . . 14 |- (U.a = X -> U.a (_ X)
4		sspwuni 2772	. . . . . . . . . . . . . . 15 |- (a (_ P~X <-> U.a (_ X)
5		visset 1820	. . . . . . . . . . . . . . . . 17 |- a e. V
6	5	elpw 2414	. . . . . . . . . . . . . . . 16 |- (a e. P~P~X <-> a (_ P~X)
7	6	biimpr 152	. . . . . . . . . . . . . . 15 |- (a (_ P~X -> a e. P~P~X)
8	4, 7	sylbir 201	. . . . . . . . . . . . . 14 |- (U.a (_ X -> a e. P~P~X)
9	3, 8	syl 10	. . . . . . . . . . . . 13 |- (U.a = X -> a e. P~P~X)
10	9	ad2antlr 407	. . . . . . . . . . . 12 |- (((a e. Fil /\ U.a = X) /\ J e. Top) -> a e. P~P~X)
11	2, 10	jca 288	. . . . . . . . . . 11 |- (((a e. Fil /\ U.a = X) /\ J e. Top) -> (a e. Fil /\ a e. P~P~X))
12		elin 2216	. . . . . . . . . . 11 |- (a e. (Fil i^i P~P~X) <-> (a e. Fil /\ a e. P~P~X))
13	11, 12	sylibr 200	. . . . . . . . . 10 |- (((a e. Fil /\ U.a = X) /\ J e. Top) -> a e. (Fil i^i P~P~X))
14	13	ex 373	. . . . . . . . 9 |- ((a e. Fil /\ U.a = X) -> (J e. Top -> a e. (Fil i^i P~P~X)))
15	14	3adant3 803	. . . . . . . 8 |- ((a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a}) -> (J e. Top -> a e. (Fil i^i P~P~X)))
16	15	impcom 351	. . . . . . 7 |- ((J e. Top /\ (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})) -> a e. (Fil i^i P~P~X))
17		3simp3 794	. . . . . . . 8 |- ((a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a}) -> b = {l e. X | ((nei` J)` {l}) (_ a})
18	17	adantl 390	. . . . . . 7 |- ((J e. Top /\ (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})) -> b = {l e. X | ((nei` J)` {l}) (_ a})
19	16, 18	jca 288	. . . . . 6 |- ((J e. Top /\ (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})) -> (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a}))
20	19	ex 373	. . . . 5 |- (J e. Top -> ((a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a}) -> (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})))
21	20	19.21aivv 1293	. . . 4 |- (J e. Top -> A.aA.b((a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a}) -> (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})))
22		ssopab2 2836	. . . 4 |- ({<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})} (_ {<.a, b>. | (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})} <-> A.aA.b((a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a}) -> (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})))
23	21, 22	sylibr 200	. . 3 |- (J e. Top -> {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})} (_ {<.a, b>. | (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})})
24		uniexg 2885	. . . . . . 7 |- (J e. Top -> U.J e. V)
25		sfvlim.1	. . . . . . 7 |- X = U.J
26	24, 25	syl5eqel 1559	. . . . . 6 |- (J e. Top -> X e. V)
27		pwexg 2760	. . . . . 6 |- (X e. V -> P~X e. V)
28		pwexg 2760	. . . . . 6 |- (P~X e. V -> P~P~X e. V)
29	26, 27, 28	3syl 20	. . . . 5 |- (J e. Top -> P~P~X e. V)
30		inex1g 2731	. . . . 5 |- (P~P~X e. V -> (P~P~X i^i Fil) e. V)
31		incom 2217	. . . . . . 7 |- (P~P~X i^i Fil) = (Fil i^i P~P~X)
32	31	eleq1i 1544	. . . . . 6 |- ((P~P~X i^i Fil) e. V <-> (Fil i^i P~P~X) e. V)
33	32	biimp 151	. . . . 5 |- ((P~P~X i^i Fil) e. V -> (Fil i^i P~P~X) e. V)
34	29, 30, 33	3syl 20	. . . 4 |- (J e. Top -> (Fil i^i P~P~X) e. V)
35		opabex2g 3625	. . . 4 |- ((Fil i^i P~P~X) e. V -> {<.a, b>. | (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})} e. V)
36	34, 35	syl 10	. . 3 |- (J e. Top -> {<.a, b>. | (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})} e. V)
37	1, 23, 36	sylanc 474	. 2 |- (J e. Top -> {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})} e. V)
38		unieq 2522	. . . . . . 7 |- (x = J -> U.x = U.J)
39	38, 25	syl6eqr 1532	. . . . . 6 |- (x = J -> U.x = X)
40	39	eqeq2d 1493	. . . . 5 |- (x = J -> (U.a = U.x <-> U.a = X))
41		rabeq 1816	. . . . . . . 8 |- (U.x = X -> {l e. U.x | ((nei` x)` {l}) (_ a} = {l e. X | ((nei` x)` {l}) (_ a})
42	39, 41	syl 10	. . . . . . 7 |- (x = J -> {l e. U.x | ((nei` x)` {l}) (_ a} = {l e. X | ((nei` x)` {l}) (_ a})
43		fveq2 3738	. . . . . . . . . 10 |- (x = J -> (nei` x) = (nei` J))
44	43	fveq1d 3740	. . . . . . . . 9 |- (x = J -> ((nei` x)` {l}) = ((nei` J)` {l}))
45	44	sseq1d 2097	. . . . . . . 8 |- (x = J -> (((nei` x)` {l}) (_ a <-> ((nei` J)` {l}) (_ a))
46	45	rabbisdv 1814	. . . . . . 7 |- (x = J -> {l e. X | ((nei` x)` {l}) (_ a} = {l e. X | ((nei` J)` {l}) (_ a})
47	42, 46	eqtrd 1514	. . . . . 6 |- (x = J -> {l e. U.x | ((nei` x)` {l}) (_ a} = {l e. X | ((nei` J)` {l}) (_ a})
48	47	eqeq2d 1493	. . . . 5 |- (x = J -> (b = {l e. U.x | ((nei` x)` {l}) (_ a} <-> b = {l e. X | ((nei` J)` {l}) (_ a}))
49	40, 48	3anbi23d 900	. . . 4 |- (x = J -> ((a e. Fil /\ U.a = U.x /\ b = {l e. U.x | ((nei` x)` {l}) (_ a}) <-> (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})))
50	49	opabbidv 2683	. . 3 |- (x = J -> {<.a, b>. | (a e. Fil /\ U.a = U.x /\ b = {l e. U.x | ((nei` x)` {l}) (_ a})} = {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})})
51		df-flim1 10594	. . 3 |- fLim1 = {<.x, y>. | (x e. Top /\ y = {<.a, b>. | (a e. Fil /\ U.a = U.x /\ b = {l e. U.x | ((nei` x)` {l}) (_ a})})}
52	50, 51	fvopab4g 3793	. 2 |- ((J e. Top /\ {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})} e. V) -> (fLim1` J) = {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)