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