Definition df-ufl 22961

Description: Define the class of base sets for which the ultrafilter lemma filssufil 22971 holds. (Contributed by Mario Carneiro, 26-Aug-2015.)

Assertion

Ref	Expression
df-ufl	⊢ UFL = {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔}

Distinct variable group:   𝑓,𝑔,𝑥

Detailed syntax breakdown of Definition df-ufl

Step	Hyp	Ref	Expression
1		cufl 22959	. 2 class UFL
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1538	. . . . . 6 class 𝑓
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1538	. . . . . 6 class 𝑔
6	3, 5	wss 3883	. . . . 5 wff 𝑓 ⊆ 𝑔
7		vx	. . . . . . 7 setvar 𝑥
8	7	cv 1538	. . . . . 6 class 𝑥
9		cufil 22958	. . . . . 6 class UFil
10	8, 9	cfv 6418	. . . . 5 class (UFil‘𝑥)
11	6, 4, 10	wrex 3064	. . . 4 wff ∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔
12		cfil 22904	. . . . 5 class Fil
13	8, 12	cfv 6418	. . . 4 class (Fil‘𝑥)
14	11, 2, 13	wral 3063	. . 3 wff ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔
15	14, 7	cab 2715	. 2 class {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔}
16	1, 15	wceq 1539	1 wff UFL = {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔}

This definition is referenced by:  isufl  22972