Metamath Proof Explorer

Theorem supfil

Description: The supersets of a nonempty set which are also subsets of a given base set form a filter. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Stefan O'Rear, 7-Aug-2015)

Ref Expression
Assertion supfil 
|- ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> { x e. ~P A | B C_ x } e. ( Fil ` A ) )

Proof

Step Hyp Ref Expression
1 sseq2 
 |-  ( x = y -> ( B C_ x <-> B C_ y ) )
2 1 elrab 
 |-  ( y e. { x e. ~P A | B C_ x } <-> ( y e. ~P A /\ B C_ y ) )
3 velpw 
 |-  ( y e. ~P A <-> y C_ A )
4 3 anbi1i 
 |-  ( ( y e. ~P A /\ B C_ y ) <-> ( y C_ A /\ B C_ y ) )
5 2 4 bitri 
 |-  ( y e. { x e. ~P A | B C_ x } <-> ( y C_ A /\ B C_ y ) )
6 5 a1i 
 |-  ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> ( y e. { x e. ~P A | B C_ x } <-> ( y C_ A /\ B C_ y ) ) )
7 simp1 
 |-  ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> A e. V )
8 simp2 
 |-  ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> B C_ A )
9 sseq2 
 |-  ( y = A -> ( B C_ y <-> B C_ A ) )
10 9 sbcieg 
 |-  ( A e. V -> ( [. A / y ]. B C_ y <-> B C_ A ) )
11 7 10 syl 
 |-  ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> ( [. A / y ]. B C_ y <-> B C_ A ) )
12 8 11 mpbird 
 |-  ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> [. A / y ]. B C_ y )
13 ss0 
 |-  ( B C_ (/) -> B = (/) )
14 13 necon3ai 
 |-  ( B =/= (/) -> -. B C_ (/) )
15 14 3ad2ant3 
 |-  ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> -. B C_ (/) )
16 0ex 
 |-  (/) e. _V
17 sseq2 
 |-  ( y = (/) -> ( B C_ y <-> B C_ (/) ) )
18 16 17 sbcie 
 |-  ( [. (/) / y ]. B C_ y <-> B C_ (/) )
19 15 18 sylnibr 
 |-  ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> -. [. (/) / y ]. B C_ y )
20 sstr 
 |-  ( ( B C_ w /\ w C_ z ) -> B C_ z )
21 20 expcom 
 |-  ( w C_ z -> ( B C_ w -> B C_ z ) )
22 vex 
 |-  w e. _V
23 sseq2 
 |-  ( y = w -> ( B C_ y <-> B C_ w ) )
24 22 23 sbcie 
 |-  ( [. w / y ]. B C_ y <-> B C_ w )
25 vex 
 |-  z e. _V
26 sseq2 
 |-  ( y = z -> ( B C_ y <-> B C_ z ) )
27 25 26 sbcie 
 |-  ( [. z / y ]. B C_ y <-> B C_ z )
28 21 24 27 3imtr4g 
 |-  ( w C_ z -> ( [. w / y ]. B C_ y -> [. z / y ]. B C_ y ) )
29 28 3ad2ant3 
 |-  ( ( ( A e. V /\ B C_ A /\ B =/= (/) ) /\ z C_ A /\ w C_ z ) -> ( [. w / y ]. B C_ y -> [. z / y ]. B C_ y ) )
30 ssin 
 |-  ( ( B C_ z /\ B C_ w ) <-> B C_ ( z i^i w ) )
31 30 biimpi 
 |-  ( ( B C_ z /\ B C_ w ) -> B C_ ( z i^i w ) )
32 27 24 31 syl2anb 
 |-  ( ( [. z / y ]. B C_ y /\ [. w / y ]. B C_ y ) -> B C_ ( z i^i w ) )
33 25 inex1 
 |-  ( z i^i w ) e. _V
34 sseq2 
 |-  ( y = ( z i^i w ) -> ( B C_ y <-> B C_ ( z i^i w ) ) )
35 33 34 sbcie 
 |-  ( [. ( z i^i w ) / y ]. B C_ y <-> B C_ ( z i^i w ) )
36 32 35 sylibr 
 |-  ( ( [. z / y ]. B C_ y /\ [. w / y ]. B C_ y ) -> [. ( z i^i w ) / y ]. B C_ y )
37 36 a1i 
 |-  ( ( ( A e. V /\ B C_ A /\ B =/= (/) ) /\ z C_ A /\ w C_ A ) -> ( ( [. z / y ]. B C_ y /\ [. w / y ]. B C_ y ) -> [. ( z i^i w ) / y ]. B C_ y ) )
38 6 7 12 19 29 37 isfild 
 |-  ( ( A e. V /\ B C_ A /\ B =/= (/) ) -> { x e. ~P A | B C_ x } e. ( Fil ` A ) )