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)

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 fdm ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → dom 𝐹 = 𝐴 )
6 dmexg ⊢ ( 𝐹 ∈ V → dom 𝐹 ∈ V )
7 6 adantr ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → dom 𝐹 ∈ V )
8 eleq1 ⊢ ( 𝐴 = dom 𝐹 → ( 𝐴 ∈ V ↔ dom 𝐹 ∈ V ) )
9 8 eqcoms ⊢ ( dom 𝐹 = 𝐴 → ( 𝐴 ∈ V ↔ dom 𝐹 ∈ V ) )
10 7 9 syl5ibr ⊢ ( dom 𝐹 = 𝐴 → ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → 𝐴 ∈ V ) )
11 1 5 10 3syl ⊢ ( 𝜑 → ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → 𝐴 ∈ V ) )
12 11 impcom ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝐴 ∈ V )
13 simplr ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑍 ∈ V )
14 elsuppfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ∧ 𝑍 ∈ V ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ) )
15 4 12 13 14 syl3anc ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ) )
16 eldif ⊢ ( 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊 ) )
17 2 adantll ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝐴 ∖ 𝑊 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
18 16 17 sylan2br ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ ( 𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ 𝑊 ) ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 )
19 18 expr ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ 𝑘 ∈ 𝑊 → ( 𝐹 ‘ 𝑘 ) = 𝑍 ) )
20 19 necon1ad ⊢ ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 → 𝑘 ∈ 𝑊 ) )
21 20 expimpd ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) → 𝑘 ∈ 𝑊 ) )
22 15 21 sylbid ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) → 𝑘 ∈ 𝑊 ) )
23 22 ssrdv ⊢ ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
24 23 ex ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 ) )
25 supp0prc ⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ∅ )
26 0ss ⊢ ∅ ⊆ 𝑊
27 25 26 eqsstrdi ⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
28 27 a1d ⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 ) )
29 24 28 pm2.61i ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )