Theorem isufl

Description: Define the (strong) ultrafilter lemma, parameterized over base sets. A set X satisfies the ultrafilter lemma if every filter on X is a subset of some ultrafilter. (Contributed by Mario Carneiro, 26-Aug-2015)

	Ref	Expression
Assertion	isufl	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ UFL ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓 ⊆ 𝑔 ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝑥 = 𝑋 → ( Fil ‘ 𝑥 ) = ( Fil ‘ 𝑋 ) )
2		fveq2	⊢ ( 𝑥 = 𝑋 → ( UFil ‘ 𝑥 ) = ( UFil ‘ 𝑋 ) )
3	2	rexeqdv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓 ⊆ 𝑔 ↔ ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓 ⊆ 𝑔 ) )
4	1 3	raleqbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑓 ∈ ( Fil ‘ 𝑥 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓 ⊆ 𝑔 ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓 ⊆ 𝑔 ) )
5		df-ufl	⊢ UFL = { 𝑥 ∣ ∀ 𝑓 ∈ ( Fil ‘ 𝑥 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑥 ) 𝑓 ⊆ 𝑔 }
6	4 5	elab2g	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 ∈ UFL ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∃ 𝑔 ∈ ( UFil ‘ 𝑋 ) 𝑓 ⊆ 𝑔 ) )