Theorem filtop

Description: The underlying set belongs to the filter. (Contributed by FL, 20-Jul-2007) (Revised by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Assertion	filtop	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		filfbas	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
2		fbasne0	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ≠ ∅ )
3	1 2	syl	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ≠ ∅ )
4		n0	⊢ ( 𝐹 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐹 )
5		filelss	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ⊆ 𝑋 )
6		ssid	⊢ 𝑋 ⊆ 𝑋
7		filss	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑋 ⊆ 𝑋 ∧ 𝑥 ⊆ 𝑋 ) ) → 𝑋 ∈ 𝐹 )
8	7	3exp2	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → ( 𝑋 ⊆ 𝑋 → ( 𝑥 ⊆ 𝑋 → 𝑋 ∈ 𝐹 ) ) ) )
9	8	imp	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑋 ⊆ 𝑋 → ( 𝑥 ⊆ 𝑋 → 𝑋 ∈ 𝐹 ) ) )
10	6 9	mpi	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ⊆ 𝑋 → 𝑋 ∈ 𝐹 ) )
11	5 10	mpd	⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ) → 𝑋 ∈ 𝐹 )
12	11	ex	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐹 → 𝑋 ∈ 𝐹 ) )
13	12	exlimdv	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ∃ 𝑥 𝑥 ∈ 𝐹 → 𝑋 ∈ 𝐹 ) )
14	4 13	biimtrid	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ≠ ∅ → 𝑋 ∈ 𝐹 ) )
15	3 14	mpd	⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )