Theorem ssfg

Description: A filter base is a subset of its generated filter. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	ssfg	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		fbelss	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑡 ∈ 𝐹 ) → 𝑡 ⊆ 𝑋 )
2	1	ex	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ 𝐹 → 𝑡 ⊆ 𝑋 ) )
3		ssid	⊢ 𝑡 ⊆ 𝑡
4		sseq1	⊢ ( 𝑥 = 𝑡 → ( 𝑥 ⊆ 𝑡 ↔ 𝑡 ⊆ 𝑡 ) )
5	4	rspcev	⊢ ( ( 𝑡 ∈ 𝐹 ∧ 𝑡 ⊆ 𝑡 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 )
6	3 5	mpan2	⊢ ( 𝑡 ∈ 𝐹 → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 )
7	2 6	jca2	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ 𝐹 → ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) ) )
8		elfg	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) ) )
9	7 8	sylibrd	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ 𝐹 → 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ) )
10	9	ssrdv	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )