Theorem fbsspw

Description: A filter base on a set is a subset of the power set. (Contributed by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Assertion	fbsspw	⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → 𝐹 ⊆ 𝒫 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → 𝐵 ∈ dom fBas )
2		isfbas	⊢ ( 𝐵 ∈ dom fBas → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
3	1 2	syl	⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ↔ ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
4	3	ibi	⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝐹 ⊆ 𝒫 𝐵 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) )
5	4	simpld	⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → 𝐹 ⊆ 𝒫 𝐵 )