Metamath Proof Explorer

Theorem filss

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

Ref Expression
Assertion filss 
|- ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> B e. F )

Proof

Step Hyp Ref Expression
1 isfil 
 |-  ( F e. ( Fil ` X ) <-> ( F e. ( fBas ` X ) /\ A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) )
2 1 simprbi 
 |-  ( F e. ( Fil ` X ) -> A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) )
3 2 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) )
4 elfvdm 
 |-  ( F e. ( Fil ` X ) -> X e. dom Fil )
5 simp2 
 |-  ( ( A e. F /\ B C_ X /\ A C_ B ) -> B C_ X )
6 elpw2g 
 |-  ( X e. dom Fil -> ( B e. ~P X <-> B C_ X ) )
7 6 biimpar 
 |-  ( ( X e. dom Fil /\ B C_ X ) -> B e. ~P X )
8 4 5 7 syl2an 
 |-  ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> B e. ~P X )
9 simpr1 
 |-  ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> A e. F )
10 simpr3 
 |-  ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> A C_ B )
11 9 10 elpwd 
 |-  ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> A e. ~P B )
12 inelcm 
 |-  ( ( A e. F /\ A e. ~P B ) -> ( F i^i ~P B ) =/= (/) )
13 9 11 12 syl2anc 
 |-  ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> ( F i^i ~P B ) =/= (/) )
14 pweq 
 |-  ( x = B -> ~P x = ~P B )
15 14 ineq2d 
 |-  ( x = B -> ( F i^i ~P x ) = ( F i^i ~P B ) )
16 15 neeq1d 
 |-  ( x = B -> ( ( F i^i ~P x ) =/= (/) <-> ( F i^i ~P B ) =/= (/) ) )
17 eleq1 
 |-  ( x = B -> ( x e. F <-> B e. F ) )
18 16 17 imbi12d 
 |-  ( x = B -> ( ( ( F i^i ~P x ) =/= (/) -> x e. F ) <-> ( ( F i^i ~P B ) =/= (/) -> B e. F ) ) )
19 18 rspccv 
 |-  ( A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) -> ( B e. ~P X -> ( ( F i^i ~P B ) =/= (/) -> B e. F ) ) )
20 3 8 13 19 syl3c 
 |-  ( ( F e. ( Fil ` X ) /\ ( A e. F /\ B C_ X /\ A C_ B ) ) -> B e. F )