Definition df-fil 10557

Description: The class of all filters. Bourbaki TG I.36 def. 1 axioms FI, FIIa, FIIb, FIII. Filters are used to define the concept of limit in the general case. It's a generalization of the idea of neighborhoods. The problem with the concept of neighborhoods is that ( in RR for instance ) you can't express the idea of a variable which tends to infinity. A work-around for this limitation is to use the idea of limit point. However limit points introduce extra sets which are fundamentally unneeded. A better idea is to use filter which succeeds in solving the problem by remaining in the studied set. Filters were invented by Cartan in 1937 and made famous by Bourbaki in his treatise. A notion similar to the notion of filter is the concept of net invented by Moore and Smith in 1922.

Assertion

Ref	Expression
df-fil	|- Fil = {f | ((-. (/) e. f /\ U.f e. f) /\ A.xA.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f) /\ A.x e. f A.y e. f (x i^i y) e. f)}

Distinct variable group:   x,f,y

Detailed syntax breakdown of Definition df-fil

Step	Hyp	Ref	Expression
1		cfil 10556	. 2 class Fil
2		c0 2280	. . . . . . 7 class (/)
3		vf	. . . . . . . 8 set f
4	3	cv 955	. . . . . . 7 class f
5	2, 4	wcel 958	. . . . . 6 wff (/) e. f
6	5	wn 2	. . . . 5 wff -. (/) e. f
7	4	cuni 2503	. . . . . 6 class U.f
8	7, 4	wcel 958	. . . . 5 wff U.f e. f
9	6, 8	wa 223	. . . 4 wff (-. (/) e. f /\ U.f e. f)
10		vx	. . . . . . . . . 10 set x
11	10	cv 955	. . . . . . . . 9 class x
12	11, 4	wcel 958	. . . . . . . 8 wff x e. f
13		vy	. . . . . . . . . 10 set y
14	13	cv 955	. . . . . . . . 9 class y
15	14, 7	wss 2047	. . . . . . . 8 wff y (_ U.f
16	11, 14	wss 2047	. . . . . . . 8 wff x (_ y
17	12, 15, 16	w3a 775	. . . . . . 7 wff (x e. f /\ y (_ U.f /\ x (_ y)
18	14, 4	wcel 958	. . . . . . 7 wff y e. f
19	17, 18	wi 3	. . . . . 6 wff ((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f)
20	19, 13	wal 954	. . . . 5 wff A.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f)
21	20, 10	wal 954	. . . 4 wff A.xA.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f)
22	11, 14	cin 2046	. . . . . . 7 class (x i^i y)
23	22, 4	wcel 958	. . . . . 6 wff (x i^i y) e. f
24	23, 13, 4	wral 1645	. . . . 5 wff A.y e. f (x i^i y) e. f
25	24, 10, 4	wral 1645	. . . 4 wff A.x e. f A.y e. f (x i^i y) e. f
26	9, 21, 25	w3a 775	. . 3 wff ((-. (/) e. f /\ U.f e. f) /\ A.xA.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f) /\ A.x e. f A.y e. f (x i^i y) e. f)
27	26, 3	cab 1463	. 2 class {f | ((-. (/) e. f /\ U.f e. f) /\ A.xA.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f) /\ A.x e. f A.y e. f (x i^i y) e. f)}
28	1, 27	wceq 956	1 wff Fil = {f | ((-. (/) e. f /\ U.f e. f) /\ A.xA.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f) /\ A.x e. f A.y e. f (x i^i y) e. f)}

This definition is referenced by:  isfil 10558

Copyright terms: Public domain