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 ‘ 𝑋 ) 𝑓 ⊆ 𝑔 ) ) |
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 ‘ 𝑋 ) 𝑓 ⊆ 𝑔 ) ) |