suppss2

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)

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

Proof

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

Metamath Proof Explorer

Theorem suppss2

Proof