Metamath Proof Explorer


Theorem isufil

Description: The property of being an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009) (Revised by Mario Carneiro, 29-Jul-2015)

Ref Expression
Assertion isufil FUFilXFFilXx𝒫XxFXxF

Proof

Step Hyp Ref Expression
1 df-ufil UFil=yVzFily|x𝒫yxzyxz
2 pweq y=X𝒫y=𝒫X
3 2 adantr y=Xz=F𝒫y=𝒫X
4 eleq2 z=FxzxF
5 4 adantl y=Xz=FxzxF
6 difeq1 y=Xyx=Xx
7 eleq12 yx=Xxz=FyxzXxF
8 6 7 sylan y=Xz=FyxzXxF
9 5 8 orbi12d y=Xz=FxzyxzxFXxF
10 3 9 raleqbidv y=Xz=Fx𝒫yxzyxzx𝒫XxFXxF
11 fveq2 y=XFily=FilX
12 fvex FilyV
13 elfvdm FFilXXdomFil
14 1 10 11 12 13 elmptrab2 FUFilXFFilXx𝒫XxFXxF