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