Theorem fmval 23769

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 23764	. . . . 5 ⊢ FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))))
2	1	a1i 11	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → FilMap = (𝑥 ∈ V, 𝑓 ∈ V ↦ (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦))))))
3		dmeq 5893	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
4	3	fveq2d 6885	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (fBas‘dom 𝑓) = (fBas‘dom 𝐹))
5	4	adantl 481	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (fBas‘dom 𝑓) = (fBas‘dom 𝐹))
6		id 22	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
7		imaeq1 6044	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (𝑓 “ 𝑦) = (𝐹 “ 𝑦))
8	7	mpteq2dv 5240	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)) = (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))
9	8	rneqd 5927	. . . . . . 7 ⊢ (𝑓 = 𝐹 → ran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)) = ran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))
10	6, 9	oveqan12d 7420	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦))) = (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))
11	5, 10	mpteq12dv 5229	. . . . 5 ⊢ ((𝑥 = 𝑋 ∧ 𝑓 = 𝐹) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))) = (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
12		fdm 6716	. . . . . . . 8 ⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌)
13	12	fveq2d 6885	. . . . . . 7 ⊢ (𝐹:𝑌⟶𝑋 → (fBas‘dom 𝐹) = (fBas‘𝑌))
14	13	mpteq1d 5233	. . . . . 6 ⊢ (𝐹:𝑌⟶𝑋 → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
15	14	3ad2ant3 1132	. . . . 5 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘dom 𝐹) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
16	11, 15	sylan9eqr 2786	. . . 4 ⊢ (((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝑥 = 𝑋 ∧ 𝑓 = 𝐹)) → (𝑏 ∈ (fBas‘dom 𝑓) ↦ (𝑥filGenran (𝑦 ∈ 𝑏 ↦ (𝑓 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
17		elex 3485	. . . . 5 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ V)
18	17	3ad2ant1 1130	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ V)
19		simp3 1135	. . . . 5 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹:𝑌⟶𝑋)
20		elfvdm 6918	. . . . . 6 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
21	20	3ad2ant2 1131	. . . . 5 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑌 ∈ dom fBas)
22	19, 21	fexd 7220	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹 ∈ V)
23		fvex 6894	. . . . . 6 ⊢ (fBas‘𝑌) ∈ V
24	23	mptex 7216	. . . . 5 ⊢ (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) ∈ V
25	24	a1i 11	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) ∈ V)
26	2, 16, 18, 22, 25	ovmpod 7552	. . 3 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑋 FilMap 𝐹) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))))
27	26	fveq1d 6883	. 2 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵))
28		mpteq1 5231	. . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)) = (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))
29	28	rneqd 5927	. . . . 5 ⊢ (𝑏 = 𝐵 → ran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)) = ran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦)))
30	29	oveq2d 7417	. . . 4 ⊢ (𝑏 = 𝐵 → (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))
31		eqid 2724	. . . 4 ⊢ (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦)))) = (𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))
32		ovex 7434	. . . 4 ⊢ (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))) ∈ V
33	30, 31, 32	fvmpt 6988	. . 3 ⊢ (𝐵 ∈ (fBas‘𝑌) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))
34	33	3ad2ant2 1131	. 2 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑏 ∈ (fBas‘𝑌) ↦ (𝑋filGenran (𝑦 ∈ 𝑏 ↦ (𝐹 “ 𝑦))))‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))
35	27, 34	eqtrd 2764	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐵) = (𝑋filGenran (𝑦 ∈ 𝐵 ↦ (𝐹 “ 𝑦))))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  Vcvv 3466   ↦ cmpt 5221  dom cdm 5666  ran crn 5667   “ cima 5669  ⟶wf 6529  ‘cfv 6533  (class class class)co 7401   ∈ cmpo 7403  fBascfbas 21216  filGencfg 21217   FilMap cfm 23759

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-fm 23764

This theorem is referenced by:  fmfil  23770  fmss  23772  elfm  23773  ucnextcn  24131  fmcfil  25122