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

Metamath Proof Explorer

Theorem suppofssd

Description: Condition for the support of a function operation to be a subset of the union of the supports of the left and right function terms. (Contributed by Steven Nguyen, 28-Aug-2023)

Ref Expression
Hypotheses suppofssd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
suppofssd.2 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
suppofssd.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
suppofssd.4 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
suppofssd.5 ⊢ ( 𝜑 → ( 𝑍 𝑋 𝑍 ) = 𝑍 )
Assertion suppofssd ( 𝜑 → ( ( 𝐹 ∘f 𝑋 𝐺 ) supp 𝑍 ) ⊆ ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 suppofssd.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 suppofssd.2 ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
3 suppofssd.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
4 suppofssd.4 ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ 𝐵 )
5 suppofssd.5 ⊢ ( 𝜑 → ( 𝑍 𝑋 𝑍 ) = 𝑍 )
6 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝑋 𝑦 ) ∈ V )
7 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
8 6 3 4 1 1 7 off ⊢ ( 𝜑 → ( 𝐹 ∘f 𝑋 𝐺 ) : 𝐴 ⟶ V )
9 eldif ⊢ ( 𝑘 ∈ ( 𝐴 ∖ ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ) ↔ ( 𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ) )
10 ioran ⊢ ( ¬ ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∨ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) ↔ ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) )
11 elun ⊢ ( 𝑘 ∈ ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ↔ ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∨ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) )
12 10 11 xchnxbir ⊢ ( ¬ 𝑘 ∈ ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ↔ ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) )
13 12 anbi2i ⊢ ( ( 𝑘 ∈ 𝐴 ∧ ¬ 𝑘 ∈ ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) ) )
14 9 13 bitri ⊢ ( 𝑘 ∈ ( 𝐴 ∖ ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) ) )
15 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
16 elsuppfn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ) )
17 15 1 2 16 syl3anc ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ) )
18 17 notbid ⊢ ( 𝜑 → ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) ↔ ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ) )
19 18 biimpd ⊢ ( 𝜑 → ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) → ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ) )
20 4 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
21 elsuppfn ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑘 ∈ ( 𝐺 supp 𝑍 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) )
22 20 1 2 21 syl3anc ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝐺 supp 𝑍 ) ↔ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) )
23 22 notbid ⊢ ( 𝜑 → ( ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ↔ ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) )
24 23 biimpd ⊢ ( 𝜑 → ( ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) → ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) )
25 19 24 anim12d ⊢ ( 𝜑 → ( ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) → ( ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ∧ ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) ) )
26 25 anim2d ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ∧ ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) ) → ( 𝑘 ∈ 𝐴 ∧ ( ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ∧ ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) ) ) )
27 26 imp ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) ) ) → ( 𝑘 ∈ 𝐴 ∧ ( ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ∧ ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) ) )
28 pm3.2 ⊢ ( 𝑘 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 → ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ) )
29 28 necon1bd ⊢ ( 𝑘 ∈ 𝐴 → ( ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝑍 ) )
30 pm3.2 ⊢ ( 𝑘 ∈ 𝐴 → ( ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 → ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) )
31 30 necon1bd ⊢ ( 𝑘 ∈ 𝐴 → ( ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = 𝑍 ) )
32 29 31 anim12d ⊢ ( 𝑘 ∈ 𝐴 → ( ( ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ∧ ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) → ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) )
33 32 imdistani ⊢ ( ( 𝑘 ∈ 𝐴 ∧ ( ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ∧ ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) ) → ( 𝑘 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) )
34 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) ) → 𝐹 Fn 𝐴 )
35 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) ) → 𝐺 Fn 𝐴 )
36 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) ) → 𝐴 ∈ 𝑉 )
37 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) ) → 𝑘 ∈ 𝐴 )
38 fnfvof ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝑘 ∈ 𝐴 ) ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝑋 ( 𝐺 ‘ 𝑘 ) ) )
39 34 35 36 37 38 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑘 ) = ( ( 𝐹 ‘ 𝑘 ) 𝑋 ( 𝐺 ‘ 𝑘 ) ) )
40 oveq12 ⊢ ( ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) → ( ( 𝐹 ‘ 𝑘 ) 𝑋 ( 𝐺 ‘ 𝑘 ) ) = ( 𝑍 𝑋 𝑍 ) )
41 40 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) ) → ( ( 𝐹 ‘ 𝑘 ) 𝑋 ( 𝐺 ‘ 𝑘 ) ) = ( 𝑍 𝑋 𝑍 ) )
42 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) ) → ( 𝑍 𝑋 𝑍 ) = 𝑍 )
43 39 41 42 3eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ( 𝐹 ‘ 𝑘 ) = 𝑍 ∧ ( 𝐺 ‘ 𝑘 ) = 𝑍 ) ) ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑘 ) = 𝑍 )
44 33 43 sylan2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑘 ) ≠ 𝑍 ) ∧ ¬ ( 𝑘 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ≠ 𝑍 ) ) ) ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑘 ) = 𝑍 )
45 27 44 syldan ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ( ¬ 𝑘 ∈ ( 𝐹 supp 𝑍 ) ∧ ¬ 𝑘 ∈ ( 𝐺 supp 𝑍 ) ) ) ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑘 ) = 𝑍 )
46 14 45 sylan2b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) ) ) → ( ( 𝐹 ∘f 𝑋 𝐺 ) ‘ 𝑘 ) = 𝑍 )
47 8 46 suppss ⊢ ( 𝜑 → ( ( 𝐹 ∘f 𝑋 𝐺 ) supp 𝑍 ) ⊆ ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) )