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∈𝒫yw∩𝒫z≠∅→z∈w∈V
3 df-fil ⊢Fil=y∈V⟼w∈fBas⁡y|∀z∈𝒫yw∩𝒫z≠∅→z∈w
4 2 3 fnmpti ⊢FilFnV
5 fnunirn ⊢FilFnV→F∈⋃ran⁡Fil↔∃x∈VF∈Fil⁡x
6 4 5 ax-mp ⊢F∈⋃ran⁡Fil↔∃x∈VF∈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∈VF∈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