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

Metamath Proof Explorer

Theorem elfg

Description: A condition for elements of a generated filter. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion elfg ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fgval ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ } )
2 1 eleq2d ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ 𝐴 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ } ) )
3 pweq ⊢ ( 𝑦 = 𝐴 → 𝒫 𝑦 = 𝒫 𝐴 )
4 3 ineq2d ⊢ ( 𝑦 = 𝐴 → ( 𝐹 ∩ 𝒫 𝑦 ) = ( 𝐹 ∩ 𝒫 𝐴 ) )
5 4 neeq1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ ↔ ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ) )
6 5 elrab ⊢ ( 𝐴 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ } ↔ ( 𝐴 ∈ 𝒫 𝑋 ∧ ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ) )
7 elfvdm ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ dom fBas )
8 elpw2g ⊢ ( 𝑋 ∈ dom fBas → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
9 7 8 syl ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
10 elin ⊢ ( 𝑥 ∈ ( 𝐹 ∩ 𝒫 𝐴 ) ↔ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ∈ 𝒫 𝐴 ) )
11 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
12 11 anbi2i ⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 ∈ 𝒫 𝐴 ) ↔ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝐴 ) )
13 10 12 bitri ⊢ ( 𝑥 ∈ ( 𝐹 ∩ 𝒫 𝐴 ) ↔ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝐴 ) )
14 13 exbii ⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝐹 ∩ 𝒫 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝐴 ) )
15 n0 ⊢ ( ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐹 ∩ 𝒫 𝐴 ) )
16 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝐴 ) )
17 14 15 16 3bitr4i ⊢ ( ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 )
18 17 a1i ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) )
19 9 18 anbi12d ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ( 𝐴 ∈ 𝒫 𝑋 ∧ ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) )
20 6 19 bitrid ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ } ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) )
21 2 20 bitrd ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) )