Description: Define the class of base sets for which the ultrafilter lemma filssufil holds. (Contributed by Mario Carneiro, 26-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-ufl | ⊢ UFL = { 𝑥 ∣ ∀ 𝑓 ∈ ( Fil ‘ 𝑥 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓 ⊆ 𝑔 } |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cufl | ⊢ UFL | |
1 | vx | ⊢ 𝑥 | |
2 | vf | ⊢ 𝑓 | |
3 | cfil | ⊢ Fil | |
4 | 1 | cv | ⊢ 𝑥 |
5 | 4 3 | cfv | ⊢ ( Fil ‘ 𝑥 ) |
6 | vg | ⊢ 𝑔 | |
7 | cufil | ⊢ UFil | |
8 | 4 7 | cfv | ⊢ ( UFil ‘ 𝑥 ) |
9 | 2 | cv | ⊢ 𝑓 |
10 | 6 | cv | ⊢ 𝑔 |
11 | 9 10 | wss | ⊢ 𝑓 ⊆ 𝑔 |
12 | 11 6 8 | wrex | ⊢ ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓 ⊆ 𝑔 |
13 | 12 2 5 | wral | ⊢ ∀ 𝑓 ∈ ( Fil ‘ 𝑥 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓 ⊆ 𝑔 |
14 | 13 1 | cab | ⊢ { 𝑥 ∣ ∀ 𝑓 ∈ ( Fil ‘ 𝑥 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓 ⊆ 𝑔 } |
15 | 0 14 | wceq | ⊢ UFL = { 𝑥 ∣ ∀ 𝑓 ∈ ( Fil ‘ 𝑥 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓 ⊆ 𝑔 } |