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 ⊢ F ∈ ⋃ ran ⁡ Fil ↔ F ∈ Fil ⁡ ⋃ F

Proof

Step Hyp Ref Expression
1 fvex ⊢ fBas ⁡ y ∈ V
2 1 rabex ⊢ w ∈ fBas ⁡ y | ∀ z ∈ 𝒫 y w ∩ 𝒫 z ≠ ∅ → z ∈ w ∈ V
3 df-fil ⊢ Fil = y ∈ V ⟼ w ∈ fBas ⁡ y | ∀ z ∈ 𝒫 y w ∩ 𝒫 z ≠ ∅ → z ∈ w
4 2 3 fnmpti ⊢ Fil Fn V
5 fnunirn ⊢ Fil Fn V → F ∈ ⋃ ran ⁡ Fil ↔ ∃ x ∈ V F ∈ Fil ⁡ x
6 4 5 ax-mp ⊢ F ∈ ⋃ ran ⁡ Fil ↔ ∃ x ∈ V F ∈ Fil ⁡ x
7 filunibas ⊢ F ∈ Fil ⁡ x → ⋃ F = x
8 7 fveq2d ⊢ F ∈ Fil ⁡ x → Fil ⁡ ⋃ F = Fil ⁡ x
9 8 eleq2d ⊢ F ∈ Fil ⁡ x → F ∈ Fil ⁡ ⋃ F ↔ F ∈ Fil ⁡ x
10 9 ibir ⊢ F ∈ Fil ⁡ x → F ∈ Fil ⁡ ⋃ F
11 10 rexlimivw ⊢ ∃ x ∈ V F ∈ Fil ⁡ x → F ∈ Fil ⁡ ⋃ F
12 6 11 sylbi ⊢ F ∈ ⋃ ran ⁡ Fil → F ∈ Fil ⁡ ⋃ F
13 fvssunirn ⊢ Fil ⁡ ⋃ F ⊆ ⋃ ran ⁡ Fil
14 13 sseli ⊢ F ∈ Fil ⁡ ⋃ F → F ∈ ⋃ ran ⁡ Fil
15 12 14 impbii ⊢ F ∈ ⋃ ran ⁡ Fil ↔ F ∈ Fil ⁡ ⋃ F