This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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