Theorem fgfil

Description: A filter generates itself. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	fgfil	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		filfbas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
2		elfg	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) ) )
3	1 2	syl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) ) )
4		filss	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑡 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑡 ) ) → 𝑡 ∈ 𝐹 )
5	4	3exp2	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → ( 𝑡 ⊆ 𝑋 → ( 𝑥 ⊆ 𝑡 → 𝑡 ∈ 𝐹 ) ) ) )
6	5	com34	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐹 ) ) ) )
7	6	rexlimdv	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐹 ) ) )
8	7	impcomd	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝑡 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝑡 ) → 𝑡 ∈ 𝐹 ) )
9	3 8	sylbid	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑡 ∈ ( 𝑋 filGen 𝐹 ) → 𝑡 ∈ 𝐹 ) )
10	9	ssrdv	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) ⊆ 𝐹 )
11		ssfg	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
12	1 11	syl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ ( 𝑋 filGen 𝐹 ) )
13	10 12	eqssd	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = 𝐹 )