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 syl5bi ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ≠ ∅ → 𝑋𝐹 ) )
15 3 14 mpd ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋𝐹 )