Metamath Proof Explorer

Theorem fmval

Description: Introduce a function that takes a function from a filtered domain to a set and produces a filter which consists of supersets of images of filter elements. The functions which are dealt with by this function are similar to nets in topology. For example, suppose we have a sequence filtered by the filter generated by its tails under the usual positive integer ordering. Then the elements of this filter are precisely the supersets of tails of this sequence. Under this definition, it is not too difficult to see that the limit of a function in the filter sense captures the notion of convergence of a sequence. As a result, the notion of a filter generalizes many ideas associated with sequences, and this function is one way to make that relationship precise in Metamath. (Contributed by Jeff Hankins, 5-Sep-2009) (Revised by Stefan O'Rear, 6-Aug-2015)

Ref Expression
Assertion fmval ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → X FilMap F ⁡ B = X filGen ran ⁡ y ∈ B ⟼ F y

Proof

Step Hyp Ref Expression
1 df-fm ⊢ FilMap = x ∈ V , f ∈ V ⟼ b ∈ fBas ⁡ dom ⁡ f ⟼ x filGen ran ⁡ y ∈ b ⟼ f y
2 1 a1i ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → FilMap = x ∈ V , f ∈ V ⟼ b ∈ fBas ⁡ dom ⁡ f ⟼ x filGen ran ⁡ y ∈ b ⟼ f y
3 dmeq ⊢ f = F → dom ⁡ f = dom ⁡ F
4 3 fveq2d ⊢ f = F → fBas ⁡ dom ⁡ f = fBas ⁡ dom ⁡ F
5 4 adantl ⊢ x = X ∧ f = F → fBas ⁡ dom ⁡ f = fBas ⁡ dom ⁡ F
6 id ⊢ x = X → x = X
7 imaeq1 ⊢ f = F → f y = F y
8 7 mpteq2dv ⊢ f = F → y ∈ b ⟼ f y = y ∈ b ⟼ F y
9 8 rneqd ⊢ f = F → ran ⁡ y ∈ b ⟼ f y = ran ⁡ y ∈ b ⟼ F y
10 6 9 oveqan12d ⊢ x = X ∧ f = F → x filGen ran ⁡ y ∈ b ⟼ f y = X filGen ran ⁡ y ∈ b ⟼ F y
11 5 10 mpteq12dv ⊢ x = X ∧ f = F → b ∈ fBas ⁡ dom ⁡ f ⟼ x filGen ran ⁡ y ∈ b ⟼ f y = b ∈ fBas ⁡ dom ⁡ F ⟼ X filGen ran ⁡ y ∈ b ⟼ F y
12 fdm ⊢ F : Y ⟶ X → dom ⁡ F = Y
13 12 fveq2d ⊢ F : Y ⟶ X → fBas ⁡ dom ⁡ F = fBas ⁡ Y
14 13 mpteq1d ⊢ F : Y ⟶ X → b ∈ fBas ⁡ dom ⁡ F ⟼ X filGen ran ⁡ y ∈ b ⟼ F y = b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y
15 14 3ad2ant3 ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → b ∈ fBas ⁡ dom ⁡ F ⟼ X filGen ran ⁡ y ∈ b ⟼ F y = b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y
16 11 15 sylan9eqr ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X ∧ x = X ∧ f = F → b ∈ fBas ⁡ dom ⁡ f ⟼ x filGen ran ⁡ y ∈ b ⟼ f y = b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y
17 elex ⊢ X ∈ A → X ∈ V
18 17 3ad2ant1 ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → X ∈ V
19 simp3 ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → F : Y ⟶ X
20 elfvdm ⊢ B ∈ fBas ⁡ Y → Y ∈ dom ⁡ fBas
21 20 3ad2ant2 ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → Y ∈ dom ⁡ fBas
22 19 21 fexd ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → F ∈ V
23 fvex ⊢ fBas ⁡ Y ∈ V
24 23 mptex ⊢ b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y ∈ V
25 24 a1i ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y ∈ V
26 2 16 18 22 25 ovmpod ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → X FilMap F = b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y
27 26 fveq1d ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → X FilMap F ⁡ B = b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y ⁡ B
28 mpteq1 ⊢ b = B → y ∈ b ⟼ F y = y ∈ B ⟼ F y
29 28 rneqd ⊢ b = B → ran ⁡ y ∈ b ⟼ F y = ran ⁡ y ∈ B ⟼ F y
30 29 oveq2d ⊢ b = B → X filGen ran ⁡ y ∈ b ⟼ F y = X filGen ran ⁡ y ∈ B ⟼ F y
31 eqid ⊢ b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y = b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y
32 ovex ⊢ X filGen ran ⁡ y ∈ B ⟼ F y ∈ V
33 30 31 32 fvmpt ⊢ B ∈ fBas ⁡ Y → b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y ⁡ B = X filGen ran ⁡ y ∈ B ⟼ F y
34 33 3ad2ant2 ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → b ∈ fBas ⁡ Y ⟼ X filGen ran ⁡ y ∈ b ⟼ F y ⁡ B = X filGen ran ⁡ y ∈ B ⟼ F y
35 27 34 eqtrd ⊢ X ∈ A ∧ B ∈ fBas ⁡ Y ∧ F : Y ⟶ X → X FilMap F ⁡ B = X filGen ran ⁡ y ∈ B ⟼ F y