suppss2f

Description: Show that the support of a function is contained in a set. (Contributed by Thierry Arnoux, 22-Jun-2017) (Revised by AV, 1-Sep-2020)

	Ref	Expression
Hypotheses	suppss2f.p	⊢ Ⅎ 𝑘 𝜑
	suppss2f.a	⊢ Ⅎ 𝑘 𝐴
	suppss2f.w	⊢ Ⅎ 𝑘 𝑊
	suppss2f.n	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 )
	suppss2f.v	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	suppss2f	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 ) ⊆ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		suppss2f.p	⊢ Ⅎ 𝑘 𝜑
2		suppss2f.a	⊢ Ⅎ 𝑘 𝐴
3		suppss2f.w	⊢ Ⅎ 𝑘 𝑊
4		suppss2f.n	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 )
5		suppss2f.v	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		nfcv	⊢ Ⅎ 𝑙 𝐴
7		nfcv	⊢ Ⅎ 𝑙 𝐵
8		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐵
9		csbeq1a	⊢ ( 𝑘 = 𝑙 → 𝐵 = ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
10	2 6 7 8 9	cbvmptf	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑙 ∈ 𝐴 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
11	10	oveq1i	⊢ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 ) = ( ( 𝑙 ∈ 𝐴 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) supp 𝑍 )
12	4	sbt	⊢ [ 𝑙 / 𝑘 ] ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 )
13		sbim	⊢ ( [ 𝑙 / 𝑘 ] ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 ) ↔ ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ) )
14		sban	⊢ ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) ↔ ( [ 𝑙 / 𝑘 ] 𝜑 ∧ [ 𝑙 / 𝑘 ] 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) )
15	1	sbf	⊢ ( [ 𝑙 / 𝑘 ] 𝜑 ↔ 𝜑 )
16	2 3	nfdif	⊢ Ⅎ 𝑘 ( 𝐴 ∖ 𝑊 )
17	16	clelsb1fw	⊢ ( [ 𝑙 / 𝑘 ] 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ↔ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) )
18	15 17	anbi12i	⊢ ( ( [ 𝑙 / 𝑘 ] 𝜑 ∧ [ 𝑙 / 𝑘 ] 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) ↔ ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) )
19	14 18	bitri	⊢ ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) ↔ ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) )
20		sbsbc	⊢ ( [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ↔ [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 )
21		sbceq1g	⊢ ( 𝑙 ∈ V → ( [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 ) )
22	21	elv	⊢ ( [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 )
23	20 22	bitri	⊢ ( [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 )
24	19 23	imbi12i	⊢ ( ( [ 𝑙 / 𝑘 ] ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → [ 𝑙 / 𝑘 ] 𝐵 = 𝑍 ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 ) )
25	13 24	bitri	⊢ ( [ 𝑙 / 𝑘 ] ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → 𝐵 = 𝑍 ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 ) )
26	12 25	mpbi	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 𝐴 ∖ 𝑊 ) ) → ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝑍 )
27	26 5	suppss2	⊢ ( 𝜑 → ( ( 𝑙 ∈ 𝐴 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) supp 𝑍 ) ⊆ 𝑊 )
28	11 27	eqsstrid	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) supp 𝑍 ) ⊆ 𝑊 )

Metamath Proof Explorer

Theorem suppss2f

Proof