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

Metamath Proof Explorer

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