This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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