Metamath Proof Explorer

Theorem filin

Description: A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion filin 
|- ( ( F e. ( Fil ` X ) /\ A e. F /\ B e. F ) -> ( A i^i B ) e. F )

Proof

Step Hyp Ref Expression
1 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
2 fbasssin 
 |-  ( ( F e. ( fBas ` X ) /\ A e. F /\ B e. F ) -> E. x e. F x C_ ( A i^i B ) )
3 1 2 syl3an1 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F /\ B e. F ) -> E. x e. F x C_ ( A i^i B ) )
4 inss1 
 |-  ( A i^i B ) C_ A
5 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> A C_ X )
6 4 5 sstrid 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( A i^i B ) C_ X )
7 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( x e. F /\ ( A i^i B ) C_ X /\ x C_ ( A i^i B ) ) ) -> ( A i^i B ) e. F )
8 7 3exp2 
 |-  ( F e. ( Fil ` X ) -> ( x e. F -> ( ( A i^i B ) C_ X -> ( x C_ ( A i^i B ) -> ( A i^i B ) e. F ) ) ) )
9 8 com23 
 |-  ( F e. ( Fil ` X ) -> ( ( A i^i B ) C_ X -> ( x e. F -> ( x C_ ( A i^i B ) -> ( A i^i B ) e. F ) ) ) )
10 9 imp 
 |-  ( ( F e. ( Fil ` X ) /\ ( A i^i B ) C_ X ) -> ( x e. F -> ( x C_ ( A i^i B ) -> ( A i^i B ) e. F ) ) )
11 10 rexlimdv 
 |-  ( ( F e. ( Fil ` X ) /\ ( A i^i B ) C_ X ) -> ( E. x e. F x C_ ( A i^i B ) -> ( A i^i B ) e. F ) )
12 6 11 syldan 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F ) -> ( E. x e. F x C_ ( A i^i B ) -> ( A i^i B ) e. F ) )
13 12 3adant3 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F /\ B e. F ) -> ( E. x e. F x C_ ( A i^i B ) -> ( A i^i B ) e. F ) )
14 3 13 mpd 
 |-  ( ( F e. ( Fil ` X ) /\ A e. F /\ B e. F ) -> ( A i^i B ) e. F )