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	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-fm	⊢ FilMap = ( 𝑥 ∈ V , 𝑓 ∈ V ↦ ( 𝑏 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) ) )
2	1	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → FilMap = ( 𝑥 ∈ V , 𝑓 ∈ V ↦ ( 𝑏 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) ) ) )
3		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
4	3	fveq2d	⊢ ( 𝑓 = 𝐹 → ( fBas ‘ dom 𝑓 ) = ( fBas ‘ dom 𝐹 ) )
5	4	adantl	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) → ( fBas ‘ dom 𝑓 ) = ( fBas ‘ dom 𝐹 ) )
6		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
7		imaeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 “ 𝑦 ) = ( 𝐹 “ 𝑦 ) )
8	7	mpteq2dv	⊢ ( 𝑓 = 𝐹 → ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) = ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) )
9	8	rneqd	⊢ ( 𝑓 = 𝐹 → ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) = ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) )
10	6 9	oveqan12d	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) → ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) )
11	5 10	mpteq12dv	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) → ( 𝑏 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) ) = ( 𝑏 ∈ ( fBas ‘ dom 𝐹 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) )
12		fdm	⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → dom 𝐹 = 𝑌 )
13	12	fveq2d	⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( fBas ‘ dom 𝐹 ) = ( fBas ‘ 𝑌 ) )
14	13	mpteq1d	⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → ( 𝑏 ∈ ( fBas ‘ dom 𝐹 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) = ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) )
15	14	3ad2ant3	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑏 ∈ ( fBas ‘ dom 𝐹 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) = ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) )
16	11 15	sylan9eqr	⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑓 = 𝐹 ) ) → ( 𝑏 ∈ ( fBas ‘ dom 𝑓 ) ↦ ( 𝑥 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝑓 “ 𝑦 ) ) ) ) = ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) )
17		elex	⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ V )
18	17	3ad2ant1	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑋 ∈ V )
19		simp3	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐹 : 𝑌 ⟶ 𝑋 )
20		elfvdm	⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝑌 ∈ dom fBas )
21	20	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝑌 ∈ dom fBas )
22	19 21	fexd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → 𝐹 ∈ V )
23		fvex	⊢ ( fBas ‘ 𝑌 ) ∈ V
24	23	mptex	⊢ ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) ∈ V
25	24	a1i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) ∈ V )
26	2 16 18 22 25	ovmpod	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑋 FilMap 𝐹 ) = ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) )
27	26	fveq1d	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) ‘ 𝐵 ) )
28		mpteq1	⊢ ( 𝑏 = 𝐵 → ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) )
29	28	rneqd	⊢ ( 𝑏 = 𝐵 → ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) = ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) )
30	29	oveq2d	⊢ ( 𝑏 = 𝐵 → ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) )
31		eqid	⊢ ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) = ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) )
32		ovex	⊢ ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) ∈ V
33	30 31 32	fvmpt	⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) ‘ 𝐵 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) )
34	33	3ad2ant2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑏 ∈ ( fBas ‘ 𝑌 ) ↦ ( 𝑋 filGen ran ( 𝑦 ∈ 𝑏 ↦ ( 𝐹 “ 𝑦 ) ) ) ) ‘ 𝐵 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) )
35	27 34	eqtrd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) = ( 𝑋 filGen ran ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 “ 𝑦 ) ) ) )