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

Theorem supfil 17965
 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 3359 . . . . 5
21elrab 3101 . . . 4
3 vex 2968 . . . . . 6
43elpw 3834 . . . . 5
54anbi1i 678 . . . 4
62, 5bitri 242 . . 3
76a1i 11 . 2
8 elex 2973 . . 3
10 simp2 959 . . 3
11 sseq2 3359 . . . . 5
1211sbcieg 3202 . . . 4
139, 12syl 16 . . 3
1410, 13mpbird 225 . 2
15 ss0 3646 . . . . 5
1615necon3ai 2651 . . . 4
18 0ex 4370 . . . 4
19 sseq2 3359 . . . 4
2018, 19sbcie 3204 . . 3
2117, 20sylnibr 298 . 2
22 sstr 3345 . . . . 5
2322expcom 426 . . . 4
24 vex 2968 . . . . 5
25 sseq2 3359 . . . . 5
2624, 25sbcie 3204 . . . 4
27 vex 2968 . . . . 5
28 sseq2 3359 . . . . 5
2927, 28sbcie 3204 . . . 4
3023, 26, 293imtr4g 263 . . 3