This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )