Description: Recover the base set from a filter. (Contributed by Stefan O'Rear, 2-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | filunibas | ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 ) |
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 ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 ) |