Theorem suppss

Description: Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019) (Proof shortened by SN, 5-Aug-2024)

	Ref	Expression
Hypotheses	suppss.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
	suppss.n	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
Assertion	suppss	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		suppss.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
2		suppss.n	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
3	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
4	3	adantl	⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝐹 Fn 𝐴 )
5		simpll	⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝐹 ∈ V )
6		simplr	⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑍 ∈ V )
7		elsuppfng	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ) )
8	4 5 6 7	syl3anc	⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ) )
9		eldif	⊢ ( 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊 ) )
10	2	adantll	⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
11	9 10	sylan2br	⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ ( 𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
12	11	expr	⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ 𝑘 ∈ 𝑊 → ( 𝐹 ‘ 𝑘 ) = 𝑍 ) )
13	12	necon1ad	⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 → 𝑘 ∈ 𝑊 ) )
14	13	expimpd	⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) → 𝑘 ∈ 𝑊 ) )
15	8 14	sylbid	⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) → 𝑘 ∈ 𝑊 ) )
16	15	ssrdv	⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
17	16	ex	⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 ) )
18		supp0prc	⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ∅ )
19		0ss	⊢ ∅ ⊆ 𝑊
20	18 19	eqsstrdi	⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
21	20	a1d	⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 ) )
22	17 21	pm2.61i	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )