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