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	$$⊢F\in \mathrm{UFil}\left(X\right)\leftrightarrow \left(F\in \mathrm{Fil}\left(X\right)\wedge \forall x\in 𝒫X\left(x\in F\vee X\setminus x\in F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ufil	$$⊢\mathrm{UFil}=\left(y\in \mathrm{V}⟼\left\{z\in \mathrm{Fil}\left(y\right)|\forall x\in 𝒫y\left(x\in z\vee y\setminus x\in z\right)\right\}\right)$$
2		pweq	$$⊢y=X\to 𝒫y=𝒫X$$
3	2	adantr	$$⊢\left(y=X\wedge z=F\right)\to 𝒫y=𝒫X$$
4		eleq2	$$⊢z=F\to \left(x\in z\leftrightarrow x\in F\right)$$
5	4	adantl	$$⊢\left(y=X\wedge z=F\right)\to \left(x\in z\leftrightarrow x\in F\right)$$
6		difeq1	$$⊢y=X\to y\setminus x=X\setminus x$$
7		eleq12	$$⊢\left(y\setminus x=X\setminus x\wedge z=F\right)\to \left(y\setminus x\in z\leftrightarrow X\setminus x\in F\right)$$
8	6 7	sylan	$$⊢\left(y=X\wedge z=F\right)\to \left(y\setminus x\in z\leftrightarrow X\setminus x\in F\right)$$
9	5 8	orbi12d	$$⊢\left(y=X\wedge z=F\right)\to \left(\left(x\in z\vee y\setminus x\in z\right)\leftrightarrow \left(x\in F\vee X\setminus x\in F\right)\right)$$
10	3 9	raleqbidv	$$⊢\left(y=X\wedge z=F\right)\to \left(\forall x\in 𝒫y\left(x\in z\vee y\setminus x\in z\right)\leftrightarrow \forall x\in 𝒫X\left(x\in F\vee X\setminus x\in F\right)\right)$$
11		fveq2	$$⊢y=X\to \mathrm{Fil}\left(y\right)=\mathrm{Fil}\left(X\right)$$
12		fvex	$$⊢\mathrm{Fil}\left(y\right)\in \mathrm{V}$$
13		elfvdm	$$⊢F\in \mathrm{Fil}\left(X\right)\to X\in \mathrm{dom}\mathrm{Fil}$$
14	1 10 11 12 13	elmptrab2	$$⊢F\in \mathrm{UFil}\left(X\right)\leftrightarrow \left(F\in \mathrm{Fil}\left(X\right)\wedge \forall x\in 𝒫X\left(x\in F\vee X\setminus x\in F\right)\right)$$