Theorem filunibas

Description: Recover the base set from a filter. (Contributed by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	filunibas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		filsspw	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
2		sspwuni	⊢ ( 𝐹 ⊆ 𝒫 𝑋 ↔ ∪ 𝐹 ⊆ 𝑋 )
3	1 2	sylib	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 ⊆ 𝑋 )
4		filtop	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
5		unissel	⊢ ( ( ∪ 𝐹 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐹 ) → ∪ 𝐹 = 𝑋 )
6	3 4 5	syl2anc	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )