Theorem fmval 23899

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.)

Assertion

Ref	Expression
fmval	⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))

Distinct variable groups:   𝑦,𝐵   𝑦,𝐹   𝑦,𝑋   𝑦,𝑌   𝑦,𝐴

Proof of Theorem fmval

Dummy variables 𝑓 𝑏 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-fm 23894	. . . . 5 ⊢ FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))))
2	1	a1i 11	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦))))))
3		dmeq 5860	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
4	3	fveq2d 6846	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (fBas‘dom 𝑓) = (fBas‘dom 𝐹))
5	4	adantl 481	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (fBas‘dom 𝑓) = (fBas‘dom 𝐹))
6		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
7		imaeq1 6022	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑓 “ 𝑦) = (𝐹 “ 𝑦))
8	7	mpteq2dv 5194	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)) = (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))
9	8	rneqd 5895	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)) = ran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))
10	6, 9	oveqan12d 7387	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦))) = (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))
11	5, 10	mpteq12dv 5187	. . . . 5 ⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))) = (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
12		fdm 6679	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌)
13	12	fveq2d 6846	. . . . . . 7 ⊢ (𝐹:𝑌⟶𝑋 → (fBas‘dom 𝐹) = (fBas‘𝑌))
14	13	mpteq1d 5190	. . . . . 6 ⊢ (𝐹:𝑌⟶𝑋 → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
15	14	3ad2ant3 1136	. . . . 5 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
16	11, 15	sylan9eqr 2794	. . . 4 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑥 = 𝑋 ∧ 𝑓 = 𝐹)) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
17		elex 3463	. . . . 5 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ V)
18	17	3ad2ant1 1134	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ V)
19		simp3 1139	. . . . 5 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹:𝑌⟶𝑋)
20		elfvdm 6876	. . . . . 6 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
21	20	3ad2ant2 1135	. . . . 5 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 ∈ dom fBas)
22	19, 21	fexd 7183	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹 ∈ V)
23		fvex 6855	. . . . . 6 ⊢ (fBas‘𝑌) ∈ V
24	23	mptex 7179	. . . . 5 ⊢ (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) ∈ V
25	24	a1i 11	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) ∈ V)
26	2, 16, 18, 22, 25	ovmpod 7520	. . 3 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
27	26	fveq1d 6844	. 2 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵))
28		mpteq1 5189	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)) = (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))
29	28	rneqd 5895	. . . . 5 ⊢ (𝑏 = 𝐵 → ran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)) = ran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))
30	29	oveq2d 7384	. . . 4 ⊢ (𝑏 = 𝐵 → (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))
31		eqid 2737	. . . 4 ⊢ (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))
32		ovex 7401	. . . 4 ⊢ (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))) ∈ V
33	30, 31, 32	fvmpt 6949	. . 3 ⊢ (𝐵 ∈ (fBas‘𝑌) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))
34	33	3ad2ant2 1135	. 2 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))
35	27, 34	eqtrd 2772	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ↦ cmpt 5181  dom cdm 5632  ran crn 5633   “ cima 5635  ⟶wf 6496  ‘cfv 6500  (class class class)co 7368   ∈ cmpo 7370  fBascfbas 21309  filGencfg 21310   FilMap cfm 23889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5226  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-fm 23894

This theorem is referenced by:  fmfil  23900  fmss  23902  elfm  23903  ucnextcn  24259  fmcfil  25240