Metamath Proof Explorer


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 ‘ 𝑋 ) → 𝐹 = 𝑋 )