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