Theorem suppss2 8142

Description: Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 22-Mar-2015.) (Revised by AV, 28-May-2019.)

Hypotheses

Ref	Expression
suppss2.n	⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍)
suppss2.a	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
suppss2	⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊)

Distinct variable groups:   𝐴,𝑘   𝜑,𝑘   𝑘,𝑊   𝑘,𝑍

Allowed substitution hints:   𝐵(𝑘)   𝑉(𝑘)

Proof of Theorem suppss2

Step	Hyp	Ref	Expression
1		eqid 2736	. . . . 5 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
2		suppss2.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3	2	adantl 481	. . . . 5 ⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝐴 ∈ 𝑉)
4		simpl 482	. . . . 5 ⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝑍 ∈ V)
5	1, 3, 4	mptsuppdifd 8128	. . . 4 ⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) = {𝑘 ∈ 𝐴 ∣ 𝐵 ∈ (V ∖ {𝑍})})
6		eldifsni 4746	. . . . . . 7 ⊢ (𝐵 ∈ (V ∖ {𝑍}) → 𝐵 ≠ 𝑍)
7		eldif 3911	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝐴 ∖ 𝑊) ↔ (𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊))
8		suppss2.n	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍)
9	8	adantll 714	. . . . . . . . . 10 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍)
10	7, 9	sylan2br 595	. . . . . . . . 9 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ (𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊)) → 𝐵 = 𝑍)
11	10	expr 456	. . . . . . . 8 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ 𝐴) → (¬ 𝑘 ∈ 𝑊 → 𝐵 = 𝑍))
12	11	necon1ad 2949	. . . . . . 7 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ 𝐴) → (𝐵 ≠ 𝑍 → 𝑘 ∈ 𝑊))
13	6, 12	syl5 34	. . . . . 6 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ 𝐴) → (𝐵 ∈ (V ∖ {𝑍}) → 𝑘 ∈ 𝑊))
14	13	3impia 1117	. . . . 5 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ 𝐴 ∧ 𝐵 ∈ (V ∖ {𝑍})) → 𝑘 ∈ 𝑊)
15	14	rabssdv 4026	. . . 4 ⊢ ((𝑍 ∈ V ∧ 𝜑) → {𝑘 ∈ 𝐴 ∣ 𝐵 ∈ (V ∖ {𝑍})} ⊆ 𝑊)
16	5, 15	eqsstrd 3968	. . 3 ⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊)
17	16	ex 412	. 2 ⊢ (𝑍 ∈ V → (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊))
18		id 22	. . . . . 6 ⊢ (¬ 𝑍 ∈ V → ¬ 𝑍 ∈ V)
19	18	intnand 488	. . . . 5 ⊢ (¬ 𝑍 ∈ V → ¬ ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V ∧ 𝑍 ∈ V))
20		supp0prc 8105	. . . . 5 ⊢ (¬ ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V ∧ 𝑍 ∈ V) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) = ∅)
21	19, 20	syl 17	. . . 4 ⊢ (¬ 𝑍 ∈ V → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) = ∅)
22		0ss 4352	. . . 4 ⊢ ∅ ⊆ 𝑊
23	21, 22	eqsstrdi 3978	. . 3 ⊢ (¬ 𝑍 ∈ V → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊)
24	23	a1d 25	. 2 ⊢ (¬ 𝑍 ∈ V → (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊))
25	17, 24	pm2.61i 182	1 ⊢ (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ≠ wne 2932  {crab 3399  Vcvv 3440   ∖ cdif 3898   ⊆ wss 3901  ∅c0 4285  {csn 4580   ↦ cmpt 5179  (class class class)co 7358   supp csupp 8102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-ov 7361  df-oprab 7362  df-mpo 7363  df-supp 8103

This theorem is referenced by:  suppsssn  8143  fsuppmptif  9302  sniffsupp  9303  cantnflem1d  9597  cantnflem1  9598  gsumzsplit  19856  gsummpt1n0  19894  gsum2dlem1  19899  gsum2dlem2  19900  gsum2d  19901  dprdfid  19948  dprdfinv  19950  dprdfadd  19951  dmdprdsplitlem  19968  dpjidcl  19989  uvcff  21746  uvcresum  21748  psrlidm  21917  psrridm  21918  mplsubrg  21960  mplmon  21990  mplmonmul  21991  mplcoe1  21992  mplcoe5  21995  mplbas2  21997  evlslem4  22031  evlslem2  22034  evlslem3  22035  evlslem1  22037  evlsvvvallem  22046  evlsvvvallem2  22047  evlsvvval  22048  coe1tmmul2  22218  coe1tmmul  22219  evls1fpws  22313  tsmssplit  24096  coe1mul3  26060  plypf1  26173  tayl0  26325  suppss2f  32716  suppss3  32802  gsummptres2  33136  gsummptfsres  33137  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnsubrunlem2  33330  elrspunidl  33509  elrspunsn  33510  fedgmullem2  33787  fldextrspunlsp  33831  evlsbagval  42812  selvvvval  42828  evlselv  42830  mhpind  42837  evlsmhpvvval  42838