Definition df-ufl 21516

Description: Define the class of base sets for which the ultrafilter lemma filssufil 21526 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 21514	. 2 class UFL
2		vf	. . . . . . 7 setvar 𝑓
3	2	cv 1474	. . . . . 6 class 𝑓
4		vg	. . . . . . 7 setvar 𝑔
5	4	cv 1474	. . . . . 6 class 𝑔
6	3, 5	wss 3540	. . . . 5 wff 𝑓 ⊆ 𝑔
7		vx	. . . . . . 7 setvar 𝑥
8	7	cv 1474	. . . . . 6 class 𝑥
9		cufil 21513	. . . . . 6 class UFil
10	8, 9	cfv 5804	. . . . 5 class (UFil‘𝑥)
11	6, 4, 10	wrex 2897	. . . 4 wff ∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔
12		cfil 21459	. . . . 5 class Fil
13	8, 12	cfv 5804	. . . 4 class (Fil‘𝑥)
14	11, 2, 13	wral 2896	. . 3 wff ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔
15	14, 7	cab 2596	. 2 class {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔}
16	1, 15	wceq 1475	1 wff UFL = {𝑥 ∣ ∀𝑓 ∈ (Fil‘𝑥)∃𝑔 ∈ (UFil‘𝑥)𝑓 ⊆ 𝑔}

This definition is referenced by:  isufl  21527