This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑍 ) ⊆ 𝑊 )