Theorem sfvlim 10605

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		simpll 412	. . . . . . . . . . . . . 14 |- (((a e. Fil /\ U.a = X) /\ J e. Top) -> a e. Fil)
2		eqimss 2109	. . . . . . . . . . . . . . . . . . 19 |- (U.a = X -> U.a (_ X)
3		sspwuni 2758	. . . . . . . . . . . . . . . . . . . 20 |- (a (_ P~X <-> U.a (_ X)
4		visset 1813	. . . . . . . . . . . . . . . . . . . . . . 23 |- a e. V
5	4	elpw 2404	. . . . . . . . . . . . . . . . . . . . . 22 |- (a e. P~P~X <-> a (_ P~X)
6	5	bicomi 172	. . . . . . . . . . . . . . . . . . . . 21 |- (a (_ P~X <-> a e. P~P~X)
7	6	biimp 151	. . . . . . . . . . . . . . . . . . . 20 |- (a (_ P~X -> a e. P~P~X)
8	3, 7	sylbir 201	. . . . . . . . . . . . . . . . . . 19 |- (U.a (_ X -> a e. P~P~X)
9	2, 8	syl 10	. . . . . . . . . . . . . . . . . 18 |- (U.a = X -> a e. P~P~X)
10	9	a1i 8	. . . . . . . . . . . . . . . . 17 |- (J e. Top -> (U.a = X -> a e. P~P~X))
11	10	com12 11	. . . . . . . . . . . . . . . 16 |- (U.a = X -> (J e. Top -> a e. P~P~X))
12	11	adantl 388	. . . . . . . . . . . . . . 15 |- ((a e. Fil /\ U.a = X) -> (J e. Top -> a e. P~P~X))
13	12	imp 350	. . . . . . . . . . . . . 14 |- (((a e. Fil /\ U.a = X) /\ J e. Top) -> a e. P~P~X)
14	1, 13	jca 288	. . . . . . . . . . . . 13 |- (((a e. Fil /\ U.a = X) /\ J e. Top) -> (a e. Fil /\ a e. P~P~X))
15		elin 2207	. . . . . . . . . . . . 13 |- (a e. (Fil i^i P~P~X) <-> (a e. Fil /\ a e. P~P~X))
16	14, 15	sylibr 200	. . . . . . . . . . . 12 |- (((a e. Fil /\ U.a = X) /\ J e. Top) -> a e. (Fil i^i P~P~X))
17	16	ex 373	. . . . . . . . . . 11 |- ((a e. Fil /\ U.a = X) -> (J e. Top -> a e. (Fil i^i P~P~X)))
18	17	3adant3 799	. . . . . . . . . 10 |- ((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)))
19	18	com12 11	. . . . . . . . 9 |- (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)))
20	19	imp 350	. . . . . . . 8 |- ((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))
21		3simp3 790	. . . . . . . . . 10 |- ((a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a}) -> b = {l e. X | ((nei` J)` {l}) (_ a})
22	21	a1i 8	. . . . . . . . 9 |- (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}))
23	22	imp 350	. . . . . . . 8 |- ((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})
24	20, 23	jca 288	. . . . . . 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) /\ b = {l e. X | ((nei` J)` {l}) (_ a}))
25	24	ex 373	. . . . . 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})))
26	25	19.21aivv 1287	. . . . 5 |- (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})))
27		ssopab2 2822	. . . . . 6 |- ({<.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})))
28	27	a1i 8	. . . . 5 |- (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})} <-> 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}))))
29	26, 28	mpbird 196	. . . 4 |- (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})})
30		uniexg 2871	. . . . . . . 8 |- (J e. Top -> U.J e. V)
31		sfvlim.1	. . . . . . . 8 |- X = U.J
32	30, 31	syl5eqel 1552	. . . . . . 7 |- (J e. Top -> X e. V)
33		pwexg 2746	. . . . . . 7 |- (X e. V -> P~X e. V)
34		pwexg 2746	. . . . . . 7 |- (P~X e. V -> P~P~X e. V)
35	32, 33, 34	3syl 20	. . . . . 6 |- (J e. Top -> P~P~X e. V)
36		inex1g 2718	. . . . . 6 |- (P~P~X e. V -> (P~P~X i^i Fil) e. V)
37		incom 2208	. . . . . . . 8 |- (P~P~X i^i Fil) = (Fil i^i P~P~X)
38	37	eleq1i 1537	. . . . . . 7 |- ((P~P~X i^i Fil) e. V <-> (Fil i^i P~P~X) e. V)
39	38	biimp 151	. . . . . 6 |- ((P~P~X i^i Fil) e. V -> (Fil i^i P~P~X) e. V)
40	35, 36, 39	3syl 20	. . . . 5 |- (J e. Top -> (Fil i^i P~P~X) e. V)
41		opabex2g 3611	. . . . 5 |- ((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)
42	40, 41	syl 10	. . . 4 |- (J e. Top -> {<.a, b>. | (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})} e. V)
43	29, 42	jca 288	. . 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})} /\ {<.a, b>. | (a e. (Fil i^i P~P~X) /\ b = {l e. X | ((nei` J)` {l}) (_ a})} e. V))
44		ssexg 2721	. . 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)
45	43, 44	syl 10	. 2 |- (J e. Top -> {<.a, b>. | (a e. Fil /\ U.a = X /\ b = {l e. X | ((nei` J)` {l}) (_ a})} e. V)
46		unieq 2510	. . . . . . 7 |- (x = J -> U.x = U.J)
47	31	eqcomi 1479	. . . . . . . 8 |- U.J = X
48	47	a1i 8	. . . . . . 7 |- (x = J -> U.J = X)
49	46, 48	eqtrd 1507	. . . . . 6 |- (x = J -> U.x = X)
50	49	eqeq2d 1486	. . . . 5 |- (x = J -> (U.a = U.x <-> U.a = X))
51		rabeq 1809	. . . . . . . 8 |- (U.x = X -> {l e. U.x | ((nei` x)` {l}) (_ a} = {l e. X | ((nei` x)` {l}) (_ a})
52	49, 51	syl 10	. . . . . . 7 |- (x = J -> {l e. U.x | ((nei` x)` {l}) (_ a} = {l e. X | ((nei` x)` {l}) (_ a})
53		fveq2 3724	. . . . . . . . . 10 |- (x = J -> (nei` x) = (nei` J))
54	53	fveq1d 3726	. . . . . . . . 9 |- (