Metamath Proof Explorer

Theorem suppfnss

Description: The support of a function which has the same zero values (in its domain) as another function is a subset of the support of this other function. (Contributed by AV, 30-Apr-2019) (Proof shortened by AV, 6-Jun-2022)

Ref Expression
Assertion suppfnss ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 simpr1 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → 𝐴 ⊆ 𝐵 )
2 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
3 2 ad2antrr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → dom 𝐹 = 𝐴 )
4 fndm ⊢ ( 𝐺 Fn 𝐵 → dom 𝐺 = 𝐵 )
5 4 ad2antlr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → dom 𝐺 = 𝐵 )
6 1 3 5 3sstr4d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → dom 𝐹 ⊆ dom 𝐺 )
7 6 adantr ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → dom 𝐹 ⊆ dom 𝐺 )
8 2 eleq2d ⊢ ( 𝐹 Fn 𝐴 → ( 𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴 ) )
9 8 ad2antrr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → ( 𝑦 ∈ dom 𝐹 ↔ 𝑦 ∈ 𝐴 ) )
10 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐺 ‘ 𝑥 ) = 𝑍 ↔ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) )
11 fveqeq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) = 𝑍 ↔ ( 𝐹 ‘ 𝑦 ) = 𝑍 ) )
12 10 11 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ↔ ( ( 𝐺 ‘ 𝑦 ) = 𝑍 → ( 𝐹 ‘ 𝑦 ) = 𝑍 ) ) )
13 12 rspcv ⊢ ( 𝑦 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( ( 𝐺 ‘ 𝑦 ) = 𝑍 → ( 𝐹 ‘ 𝑦 ) = 𝑍 ) ) )
14 9 13 syl6bi ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → ( 𝑦 ∈ dom 𝐹 → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( ( 𝐺 ‘ 𝑦 ) = 𝑍 → ( 𝐹 ‘ 𝑦 ) = 𝑍 ) ) ) )
15 14 com23 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝑦 ∈ dom 𝐹 → ( ( 𝐺 ‘ 𝑦 ) = 𝑍 → ( 𝐹 ‘ 𝑦 ) = 𝑍 ) ) ) )
16 15 imp31 ⊢ ( ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐺 ‘ 𝑦 ) = 𝑍 → ( 𝐹 ‘ 𝑦 ) = 𝑍 ) )
17 16 necon3d ⊢ ( ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑦 ) ≠ 𝑍 → ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 ) )
18 17 ex ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝑦 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝑦 ) ≠ 𝑍 → ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 ) ) )
19 18 com23 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( ( 𝐹 ‘ 𝑦 ) ≠ 𝑍 → ( 𝑦 ∈ dom 𝐹 → ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 ) ) )
20 19 3imp ⊢ ( ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) ∧ ( 𝐹 ‘ 𝑦 ) ≠ 𝑍 ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 )
21 7 20 rabssrabd ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ≠ 𝑍 } ⊆ { 𝑦 ∈ dom 𝐺 ∣ ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 } )
22 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
23 22 ad2antrr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → Fun 𝐹 )
24 simpl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → 𝐹 Fn 𝐴 )
25 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V )
26 25 3adant3 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝐴 ∈ V )
27 fnex ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ V ) → 𝐹 ∈ V )
28 24 26 27 syl2an ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → 𝐹 ∈ V )
29 simpr3 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → 𝑍 ∈ 𝑊 )
30 suppval1 ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ≠ 𝑍 } )
31 23 28 29 30 syl3anc ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → ( 𝐹 supp 𝑍 ) = { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ≠ 𝑍 } )
32 fnfun ⊢ ( 𝐺 Fn 𝐵 → Fun 𝐺 )
33 32 ad2antlr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → Fun 𝐺 )
34 simpr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) → 𝐺 Fn 𝐵 )
35 simp2 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝐵 ∈ 𝑉 )
36 fnex ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐺 ∈ V )
37 34 35 36 syl2an ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → 𝐺 ∈ V )
38 suppval1 ⊢ ( ( Fun 𝐺 ∧ 𝐺 ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( 𝐺 supp 𝑍 ) = { 𝑦 ∈ dom 𝐺 ∣ ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 } )
39 33 37 29 38 syl3anc ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → ( 𝐺 supp 𝑍 ) = { 𝑦 ∈ dom 𝐺 ∣ ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 } )
40 31 39 sseq12d ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → ( ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) ↔ { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ≠ 𝑍 } ⊆ { 𝑦 ∈ dom 𝐺 ∣ ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 } ) )
41 40 adantr ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) ↔ { 𝑦 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑦 ) ≠ 𝑍 } ⊆ { 𝑦 ∈ dom 𝐺 ∣ ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 } ) )
42 21 41 mpbird ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )
43 42 ex ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ) → ( ∀ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) ) )