Metamath Proof Explorer


Definition df-ufl

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 ‘ 𝑥 ) 𝑓𝑔 }

Detailed syntax breakdown

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 ‘ 𝑥 ) 𝑓𝑔 }