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

Metamath Proof Explorer

Theorem fgval

Description: The filter generating class gives a filter for every filter base. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fgval 
|- ( F e. ( fBas ` X ) -> ( X filGen F ) = { x e. ~P X | ( F i^i ~P x ) =/= (/) } )

Proof

Step Hyp Ref Expression
1 df-fg 
 |-  filGen = ( v e. _V , f e. ( fBas ` v ) |-> { x e. ~P v | ( f i^i ~P x ) =/= (/) } )
2 1 a1i 
 |-  ( F e. ( fBas ` X ) -> filGen = ( v e. _V , f e. ( fBas ` v ) |-> { x e. ~P v | ( f i^i ~P x ) =/= (/) } ) )
3 pweq 
 |-  ( v = X -> ~P v = ~P X )
4 3 adantr 
 |-  ( ( v = X /\ f = F ) -> ~P v = ~P X )
5 ineq1 
 |-  ( f = F -> ( f i^i ~P x ) = ( F i^i ~P x ) )
6 5 neeq1d 
 |-  ( f = F -> ( ( f i^i ~P x ) =/= (/) <-> ( F i^i ~P x ) =/= (/) ) )
7 6 adantl 
 |-  ( ( v = X /\ f = F ) -> ( ( f i^i ~P x ) =/= (/) <-> ( F i^i ~P x ) =/= (/) ) )
8 4 7 rabeqbidv 
 |-  ( ( v = X /\ f = F ) -> { x e. ~P v | ( f i^i ~P x ) =/= (/) } = { x e. ~P X | ( F i^i ~P x ) =/= (/) } )
9 8 adantl 
 |-  ( ( F e. ( fBas ` X ) /\ ( v = X /\ f = F ) ) -> { x e. ~P v | ( f i^i ~P x ) =/= (/) } = { x e. ~P X | ( F i^i ~P x ) =/= (/) } )
10 fveq2 
 |-  ( v = X -> ( fBas ` v ) = ( fBas ` X ) )
11 10 adantl 
 |-  ( ( F e. ( fBas ` X ) /\ v = X ) -> ( fBas ` v ) = ( fBas ` X ) )
12 elfvex 
 |-  ( F e. ( fBas ` X ) -> X e. _V )
13 id 
 |-  ( F e. ( fBas ` X ) -> F e. ( fBas ` X ) )
14 elfvdm 
 |-  ( F e. ( fBas ` X ) -> X e. dom fBas )
15 pwexg 
 |-  ( X e. dom fBas -> ~P X e. _V )
16 rabexg 
 |-  ( ~P X e. _V -> { x e. ~P X | ( F i^i ~P x ) =/= (/) } e. _V )
17 14 15 16 3syl 
 |-  ( F e. ( fBas ` X ) -> { x e. ~P X | ( F i^i ~P x ) =/= (/) } e. _V )
18 2 9 11 12 13 17 ovmpodx 
 |-  ( F e. ( fBas ` X ) -> ( X filGen F ) = { x e. ~P X | ( F i^i ~P x ) =/= (/) } )