Metamath Proof Explorer


Theorem isfil

Description: The predicate "is a filter." (Contributed by FL, 20-Jul-2007) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion isfil FFilXFfBasXx𝒫XF𝒫xxF

Proof

Step Hyp Ref Expression
1 df-fil Fil=zVffBasz|x𝒫zf𝒫xxf
2 pweq z=X𝒫z=𝒫X
3 2 adantr z=Xf=F𝒫z=𝒫X
4 ineq1 f=Ff𝒫x=F𝒫x
5 4 neeq1d f=Ff𝒫xF𝒫x
6 eleq2 f=FxfxF
7 5 6 imbi12d f=Ff𝒫xxfF𝒫xxF
8 7 adantl z=Xf=Ff𝒫xxfF𝒫xxF
9 3 8 raleqbidv z=Xf=Fx𝒫zf𝒫xxfx𝒫XF𝒫xxF
10 fveq2 z=XfBasz=fBasX
11 fvex fBaszV
12 elfvdm FfBasXXdomfBas
13 1 9 10 11 12 elmptrab2 FFilXFfBasXx𝒫XF𝒫xxF