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

Metamath Proof Explorer

Theorem elfilss

Description: An element belongs to a filter iff any element below it does. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion elfilss ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝐹 ↔ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 ibar ⊢ ( 𝐴 ⊆ 𝑋 → ( ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
2 1 adantl ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
3 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
4 elfg ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
5 3 4 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
6 5 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) ) )
7 fgfil ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = 𝐹 )
8 7 eleq2d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ 𝐴 ∈ 𝐹 ) )
9 8 adantr ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ 𝐴 ∈ 𝐹 ) )
10 2 6 9 3bitr2rd ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 ∈ 𝐹 ↔ ∃ 𝑡 ∈ 𝐹 𝑡 ⊆ 𝐴 ) )