Definition df-fbas 14104

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.)

Assertion

Ref	Expression
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 ) ) =/= (/) ) } )

Distinct variable group:   x, y, z, w

Detailed syntax breakdown of Definition df-fbas

Step	Hyp	Ref	Expression
1		cfbas 14095	. 2 class fBas
2		vw	. . 3 setvar w
3		cvv 2763	. . 3 class _V
4		vx	. . . . . . 7 setvar x
5	4	cv 1363	. . . . . 6 class x
6		c0 3450	. . . . . 6 class (/)
7	5, 6	wne 2367	. . . . 5 wff x =/= (/)
8	6, 5	wnel 2462	. . . . 5 wff (/) e/ x
9		vy	. . . . . . . . . . . 12 setvar y
10	9	cv 1363	. . . . . . . . . . 11 class y
11		vz	. . . . . . . . . . . 12 setvar z
12	11	cv 1363	. . . . . . . . . . 11 class z
13	10, 12	cin 3156	. . . . . . . . . 10 class ( y i^i z )
14	13	cpw 3605	. . . . . . . . 9 class ~P ( y i^i z )
15	5, 14	cin 3156	. . . . . . . 8 class ( x i^i ~P ( y i^i z ) )
16	15, 6	wne 2367	. . . . . . 7 wff ( x i^i ~P ( y i^i z ) ) =/= (/)
17	16, 11, 5	wral 2475	. . . . . 6 wff A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/)
18	17, 9, 5	wral 2475	. . . . 5 wff A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/)
19	7, 8, 18	w3a 980	. . . 4 wff ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) )
20	2	cv 1363	. . . . . 6 class w
21	20	cpw 3605	. . . . 5 class ~P w
22	21	cpw 3605	. . . 4 class ~P ~P w
23	19, 4, 22	crab 2479	. . 3 class { 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	2, 3, 23	cmpt 4094	. 2 class ( 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 ) ) =/= (/) ) } )
25	1, 24	wceq 1364	1 wff 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 ) ) =/= (/) ) } )

This definition is referenced by: (None)