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

Metamath Proof Explorer

Theorem filunirn

Description: Two ways to express a filter on an unspecified base. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion filunirn ( 𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( fBas ‘ 𝑦 ) ∈ V
2 1 rabex ⊢ { 𝑤 ∈ ( fBas ‘ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝒫 𝑦 ( ( 𝑤 ∩ 𝒫 𝑧 ) ≠ ∅ → 𝑧 ∈ 𝑤 ) } ∈ V
3 df-fil ⊢ Fil = ( 𝑦 ∈ V ↦ { 𝑤 ∈ ( fBas ‘ 𝑦 ) ∣ ∀ 𝑧 ∈ 𝒫 𝑦 ( ( 𝑤 ∩ 𝒫 𝑧 ) ≠ ∅ → 𝑧 ∈ 𝑤 ) } )
4 2 3 fnmpti ⊢ Fil Fn V
5 fnunirn ⊢ ( Fil Fn V → ( 𝐹 ∈ ∪ ran Fil ↔ ∃ 𝑥 ∈ V 𝐹 ∈ ( Fil ‘ 𝑥 ) ) )
6 4 5 ax-mp ⊢ ( 𝐹 ∈ ∪ ran Fil ↔ ∃ 𝑥 ∈ V 𝐹 ∈ ( Fil ‘ 𝑥 ) )
7 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑥 ) → ∪ 𝐹 = 𝑥 )
8 7 fveq2d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑥 ) → ( Fil ‘ ∪ 𝐹 ) = ( Fil ‘ 𝑥 ) )
9 8 eleq2d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑥 ) → ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ↔ 𝐹 ∈ ( Fil ‘ 𝑥 ) ) )
10 9 ibir ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑥 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
11 10 rexlimivw ⊢ ( ∃ 𝑥 ∈ V 𝐹 ∈ ( Fil ‘ 𝑥 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
12 6 11 sylbi ⊢ ( 𝐹 ∈ ∪ ran Fil → 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
13 fvssunirn ⊢ ( Fil ‘ ∪ 𝐹 ) ⊆ ∪ ran Fil
14 13 sseli ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → 𝐹 ∈ ∪ ran Fil )
15 12 14 impbii ⊢ ( 𝐹 ∈ ∪ ran Fil ↔ 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )