Theorem suppss2 8179

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 2733	. . . . 5 ⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵)
2		suppss2.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
3	2	adantl 483	. . . . 5 ⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝐴 ∈ 𝑉)
4		simpl 484	. . . . 5 ⊢ ((𝑍 ∈ V ∧ 𝜑) → 𝑍 ∈ V)
5	1, 3, 4	mptsuppdifd 8165	. . . 4 ⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) = {𝑘 ∈ 𝐴 ∣ 𝐵 ∈ (V ∖ {𝑍})})
6		eldifsni 4791	. . . . . . 7 ⊢ (𝐵 ∈ (V ∖ {𝑍}) → 𝐵 ≠ 𝑍)
7		eldif 3956	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝐴 ∖ 𝑊) ↔ (𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊))
8		suppss2.n	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍)
9	8	adantll 713	. . . . . . . . . 10 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ (𝐴 ∖ 𝑊)) → 𝐵 = 𝑍)
10	7, 9	sylan2br 596	. . . . . . . . 9 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ (𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊)) → 𝐵 = 𝑍)
11	10	expr 458	. . . . . . . 8 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ 𝐴) → (¬ 𝑘 ∈ 𝑊 → 𝐵 = 𝑍))
12	11	necon1ad 2958	. . . . . . 7 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ 𝐴) → (𝐵 ≠ 𝑍 → 𝑘 ∈ 𝑊))
13	6, 12	syl5 34	. . . . . 6 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ 𝐴) → (𝐵 ∈ (V ∖ {𝑍}) → 𝑘 ∈ 𝑊))
14	13	3impia 1118	. . . . 5 ⊢ (((𝑍 ∈ V ∧ 𝜑) ∧ 𝑘 ∈ 𝐴 ∧ 𝐵 ∈ (V ∖ {𝑍})) → 𝑘 ∈ 𝑊)
15	14	rabssdv 4070	. . . 4 ⊢ ((𝑍 ∈ V ∧ 𝜑) → {𝑘 ∈ 𝐴 ∣ 𝐵 ∈ (V ∖ {𝑍})} ⊆ 𝑊)
16	5, 15	eqsstrd 4018	. . 3 ⊢ ((𝑍 ∈ V ∧ 𝜑) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊)
17	16	ex 414	. 2 ⊢ (𝑍 ∈ V → (𝜑 → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) ⊆ 𝑊))
18		id 22	. . . . . 6 ⊢ (¬ 𝑍 ∈ V → ¬ 𝑍 ∈ V)
19	18	intnand 490	. . . . 5 ⊢ (¬ 𝑍 ∈ V → ¬ ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V ∧ 𝑍 ∈ V))
20		supp0prc 8143	. . . . 5 ⊢ (¬ ((𝑘 ∈ 𝐴 ↦ 𝐵) ∈ V ∧ 𝑍 ∈ V) → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) = ∅)
21	19, 20	syl 17	. . . 4 ⊢ (¬ 𝑍 ∈ V → ((𝑘 ∈ 𝐴 ↦ 𝐵) supp 𝑍) = ∅)
22		0ss 4394	. . . 4 ⊢ ∅ ⊆ 𝑊
23	21, 22	eqsstrdi 4034	. . 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 397   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  {crab 3433  Vcvv 3475   ∖ cdif 3943   ⊆ wss 3946  ∅c0 4320  {csn 4626   ↦ cmpt 5229  (class class class)co 7403   supp csupp 8140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5283  ax-sep 5297  ax-nul 5304  ax-pr 5425  ax-un 7719

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4907  df-iun 4997  df-br 5147  df-opab 5209  df-mpt 5230  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-iota 6491  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7406  df-oprab 7407  df-mpo 7408  df-supp 8141

This theorem is referenced by:  suppsssn  8180  fsuppmptif  9389  sniffsupp  9390  cantnflem1d  9678  cantnflem1  9679  gsumzsplit  19786  gsummpt1n0  19824  gsum2dlem1  19829  gsum2dlem2  19830  gsum2d  19831  dprdfid  19878  dprdfinv  19880  dprdfadd  19881  dmdprdsplitlem  19898  dpjidcl  19919  uvcff  21329  uvcresum  21331  psrbagaddclOLD  21463  psrlidm  21504  psrridm  21505  mplsubrg  21545  mplmon  21571  mplmonmul  21572  mplcoe1  21573  mplcoe5  21576  mplbas2  21578  evlslem4  21618  evlslem2  21623  evlslem3  21624  evlslem1  21626  coe1tmmul2  21779  coe1tmmul  21780  tsmssplit  23637  coe1mul3  25598  plypf1  25707  tayl0  25855  suppss2f  31840  suppss3  31926  gsummptres2  32182  elrspunidl  32503  elrspunsn  32504  evls1fpws  32595  fedgmullem2  32659  evlsvvvallem  41082  evlsvvvallem2  41083  evlsvvval  41084  evlsbagval  41087  selvvvval  41106  evlselv  41108  mhpind  41115  evlsmhpvvval  41116