Theorem filunirn

Description: Two ways to express a filter on an unspecified base. (Contributed by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	filunirn	|- ( F e. U. ran Fil <-> F e. ( Fil ` U. F ) )

Proof

Step	Hyp	Ref	Expression
1		fvex	|- ( fBas ` y ) e. _V
2	1	rabex	|- { w e. ( fBas ` y ) | A. z e. ~P y ( ( w i^i ~P z ) =/= (/) -> z e. w ) } e. _V
3		df-fil	|- Fil = ( y e. _V |-> { w e. ( fBas ` y ) | A. z e. ~P y ( ( w i^i ~P z ) =/= (/) -> z e. w ) } )
4	2 3	fnmpti	|- Fil Fn _V
5		fnunirn	|- ( Fil Fn _V -> ( F e. U. ran Fil <-> E. x e. _V F e. ( Fil ` x ) ) )
6	4 5	ax-mp	|- ( F e. U. ran Fil <-> E. x e. _V F e. ( Fil ` x ) )
7		filunibas	|- ( F e. ( Fil ` x ) -> U. F = x )
8	7	fveq2d	|- ( F e. ( Fil ` x ) -> ( Fil ` U. F ) = ( Fil ` x ) )
9	8	eleq2d	|- ( F e. ( Fil ` x ) -> ( F e. ( Fil ` U. F ) <-> F e. ( Fil ` x ) ) )
10	9	ibir	|- ( F e. ( Fil ` x ) -> F e. ( Fil ` U. F ) )
11	10	rexlimivw	|- ( E. x e. _V F e. ( Fil ` x ) -> F e. ( Fil ` U. F ) )
12	6 11	sylbi	|- ( F e. U. ran Fil -> F e. ( Fil ` U. F ) )
13		fvssunirn	|- ( Fil ` U. F ) C_ U. ran Fil
14	13	sseli	|- ( F e. ( Fil ` U. F ) -> F e. U. ran Fil )
15	12 14	impbii	|- ( F e. U. ran Fil <-> F e. ( Fil ` U. F ) )