This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝐵 ) ) → 𝐵 ∈ 𝐹 )

Proof

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