Metamath Proof Explorer


Theorem isufl

Description: Define the (strong) ultrafilter lemma, parameterized over base sets. A set X satisfies the ultrafilter lemma if every filter on X is a subset of some ultrafilter. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion isufl ( 𝑋𝑉 → ( 𝑋 ∈ UFL ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓𝑔 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ( 𝑥 = 𝑋 → ( Fil ‘ 𝑥 ) = ( Fil ‘ 𝑋 ) )
2 fveq2 ( 𝑥 = 𝑋 → ( UFil ‘ 𝑥 ) = ( UFil ‘ 𝑋 ) )
3 2 rexeqdv ( 𝑥 = 𝑋 → ( ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓𝑔 ↔ ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓𝑔 ) )
4 1 3 raleqbidv ( 𝑥 = 𝑋 → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑥 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓𝑔 ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓𝑔 ) )
5 df-ufl UFL = { 𝑥 ∣ ∀ 𝑓 ∈ ( Fil ‘ 𝑥 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓𝑔 }
6 4 5 elab2g ( 𝑋𝑉 → ( 𝑋 ∈ UFL ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓𝑔 ) )