Metamath Proof Explorer

Theorem filss

Description: A filter is closed under taking supersets. (Contributed by FL, 20-Jul-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion filss ⊢ F ∈ Fil ⁡ X ∧ A ∈ F ∧ B ⊆ X ∧ A ⊆ B → B ∈ F

Proof

Step Hyp Ref Expression
1 isfil ⊢ F ∈ Fil ⁡ X ↔ F ∈ fBas ⁡ X ∧ ∀ x ∈ 𝒫 X F ∩ 𝒫 x ≠ ∅ → x ∈ F
2 1 simprbi ⊢ F ∈ Fil ⁡ X → ∀ x ∈ 𝒫 X F ∩ 𝒫 x ≠ ∅ → x ∈ F
3 2 adantr ⊢ F ∈ Fil ⁡ X ∧ A ∈ F ∧ B ⊆ X ∧ A ⊆ B → ∀ x ∈ 𝒫 X F ∩ 𝒫 x ≠ ∅ → x ∈ F
4 elfvdm ⊢ F ∈ Fil ⁡ X → X ∈ dom ⁡ Fil
5 simp2 ⊢ A ∈ F ∧ B ⊆ X ∧ A ⊆ B → B ⊆ X
6 elpw2g ⊢ X ∈ dom ⁡ Fil → B ∈ 𝒫 X ↔ B ⊆ X
7 6 biimpar ⊢ X ∈ dom ⁡ Fil ∧ B ⊆ X → B ∈ 𝒫 X
8 4 5 7 syl2an ⊢ F ∈ Fil ⁡ X ∧ A ∈ F ∧ B ⊆ X ∧ A ⊆ B → B ∈ 𝒫 X
9 simpr1 ⊢ F ∈ Fil ⁡ X ∧ A ∈ F ∧ B ⊆ X ∧ A ⊆ B → A ∈ F
10 simpr3 ⊢ F ∈ Fil ⁡ X ∧ A ∈ F ∧ B ⊆ X ∧ A ⊆ B → A ⊆ B
11 9 10 elpwd ⊢ F ∈ Fil ⁡ X ∧ A ∈ F ∧ B ⊆ X ∧ A ⊆ B → A ∈ 𝒫 B
12 inelcm ⊢ A ∈ F ∧ A ∈ 𝒫 B → F ∩ 𝒫 B ≠ ∅
13 9 11 12 syl2anc ⊢ F ∈ Fil ⁡ X ∧ A ∈ F ∧ B ⊆ X ∧ A ⊆ B → F ∩ 𝒫 B ≠ ∅
14 pweq ⊢ x = B → 𝒫 x = 𝒫 B
15 14 ineq2d ⊢ x = B → F ∩ 𝒫 x = F ∩ 𝒫 B
16 15 neeq1d ⊢ x = B → F ∩ 𝒫 x ≠ ∅ ↔ F ∩ 𝒫 B ≠ ∅
17 eleq1 ⊢ x = B → x ∈ F ↔ B ∈ F
18 16 17 imbi12d ⊢ x = B → F ∩ 𝒫 x ≠ ∅ → x ∈ F ↔ F ∩ 𝒫 B ≠ ∅ → B ∈ F
19 18 rspccv ⊢ ∀ x ∈ 𝒫 X F ∩ 𝒫 x ≠ ∅ → x ∈ F → B ∈ 𝒫 X → F ∩ 𝒫 B ≠ ∅ → B ∈ F
20 3 8 13 19 syl3c ⊢ F ∈ Fil ⁡ X ∧ A ∈ F ∧ B ⊆ X ∧ A ⊆ B → B ∈ F