Definition df-fbas

Description: Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 11-Jul-2015)

	Ref	Expression
Assertion	df-fbas	|- fBas = ( w e. _V |-> { x e. ~P ~P w | ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfbas	|- fBas
1		vw	|- w
2		cvv	|- _V
3		vx	|- x
4	1	cv	|- w
5	4	cpw	|- ~P w
6	5	cpw	|- ~P ~P w
7	3	cv	|- x
8		c0	|- (/)
9	7 8	wne	|- x =/= (/)
10	8 7	wnel	|- (/) e/ x
11		vy	|- y
12		vz	|- z
13	11	cv	|- y
14	12	cv	|- z
15	13 14	cin	|- ( y i^i z )
16	15	cpw	|- ~P ( y i^i z )
17	7 16	cin	|- ( x i^i ~P ( y i^i z ) )
18	17 8	wne	|- ( x i^i ~P ( y i^i z ) ) =/= (/)
19	18 12 7	wral	|- A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/)
20	19 11 7	wral	|- A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/)
21	9 10 20	w3a	|- ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) )
22	21 3 6	crab	|- { x e. ~P ~P w | ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) ) }
23	1 2 22	cmpt	|- ( w e. _V |-> { x e. ~P ~P w | ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) ) } )
24	0 23	wceq	|- fBas = ( w e. _V |-> { x e. ~P ~P w | ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) ) } )