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 )