Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  supfil Structured version   Visualization version   Unicode version

Theorem supfil 20903
 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.)
Assertion
Ref Expression
supfil
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem supfil
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq2 3453 . . . . 5
21elrab 3195 . . . 4
3 selpw 3957 . . . . 5
43anbi1i 700 . . . 4
52, 4bitri 253 . . 3
65a1i 11 . 2
7 elex 3053 . . 3
9 simp2 1008 . . 3
10 sseq2 3453 . . . . 5
1110sbcieg 3299 . . . 4
128, 11syl 17 . . 3
139, 12mpbird 236 . 2
14 ss0 3764 . . . . 5
1514necon3ai 2648 . . . 4
17 0ex 4534 . . . 4
18 sseq2 3453 . . . 4
1917, 18sbcie 3301 . . 3
2016, 19sylnibr 307 . 2
21 sstr 3439 . . . . 5
2221expcom 437 . . . 4
23 vex 3047 . . . . 5
24 sseq2 3453 . . . . 5
2523, 24sbcie 3301 . . . 4
26 vex 3047 . . . . 5
27 sseq2 3453 . . . . 5
2826, 27sbcie 3301 . . . 4
2922, 25, 283imtr4g 274 . . 3