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	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-ufil	⊢ UFil = ( 𝑦 ∈ V ↦ { 𝑧 ∈ ( Fil ‘ 𝑦 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑦 ( 𝑥 ∈ 𝑧 ∨ ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ) } )
2		pweq	⊢ ( 𝑦 = 𝑋 → 𝒫 𝑦 = 𝒫 𝑋 )
3	2	adantr	⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → 𝒫 𝑦 = 𝒫 𝑋 )
4		eleq2	⊢ ( 𝑧 = 𝐹 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐹 ) )
5	4	adantl	⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐹 ) )
6		difeq1	⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∖ 𝑥 ) = ( 𝑋 ∖ 𝑥 ) )
7		eleq12	⊢ ( ( ( 𝑦 ∖ 𝑥 ) = ( 𝑋 ∖ 𝑥 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
8	6 7	sylan	⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → ( ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
9	5 8	orbi12d	⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝑧 ∨ ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ) ↔ ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) )
10	3 9	raleqbidv	⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → ( ∀ 𝑥 ∈ 𝒫 𝑦 ( 𝑥 ∈ 𝑧 ∨ ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) )
11		fveq2	⊢ ( 𝑦 = 𝑋 → ( Fil ‘ 𝑦 ) = ( Fil ‘ 𝑋 ) )
12		fvex	⊢ ( Fil ‘ 𝑦 ) ∈ V
13		elfvdm	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ dom Fil )
14	1 10 11 12 13	elmptrab2	⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) )