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 φ A V
suppofssd.2 φ Z B
suppofssd.3 φ F : A B
suppofssd.4 φ G : A B
suppofssd.5 φ Z X Z = Z
Assertion suppofssd φ F X f G supp Z supp Z F supp Z G

Proof

Step Hyp Ref Expression
1 suppofssd.1 φ A V
2 suppofssd.2 φ Z B
3 suppofssd.3 φ F : A B
4 suppofssd.4 φ G : A B
5 suppofssd.5 φ Z X Z = Z
6 ovexd φ x B y B x X y V
7 inidm A A = A
8 6 3 4 1 1 7 off φ F X f G : A V
9 eldif k A supp Z F supp Z G k A ¬ k supp Z F supp Z G
10 ioran ¬ k supp Z F k supp Z G ¬ k supp Z F ¬ k supp Z G
11 elun k supp Z F supp Z G k supp Z F k supp Z G
12 10 11 xchnxbir ¬ k supp Z F supp Z G ¬ k supp Z F ¬ k supp Z G
13 12 anbi2i k A ¬ k supp Z F supp Z G k A ¬ k supp Z F ¬ k supp Z G
14 9 13 bitri k A supp Z F supp Z G k A ¬ k supp Z F ¬ k supp Z G
15 3 ffnd φ F Fn A
16 elsuppfn F Fn A A V Z B k supp Z F k A F k Z
17 15 1 2 16 syl3anc φ k supp Z F k A F k Z
18 17 notbid φ ¬ k supp Z F ¬ k A F k Z
19 18 biimpd φ ¬ k supp Z F ¬ k A F k Z
20 4 ffnd φ G Fn A
21 elsuppfn G Fn A A V Z B k supp Z G k A G k Z
22 20 1 2 21 syl3anc φ k supp Z G k A G k Z
23 22 notbid φ ¬ k supp Z G ¬ k A G k Z
24 23 biimpd φ ¬ k supp Z G ¬ k A G k Z
25 19 24 anim12d φ ¬ k supp Z F ¬ k supp Z G ¬ k A F k Z ¬ k A G k Z
26 25 anim2d φ k A ¬ k supp Z F ¬ k supp Z G k A ¬ k A F k Z ¬ k A G k Z
27 26 imp φ k A ¬ k supp Z F ¬ k supp Z G k A ¬ k A F k Z ¬ k A G k Z
28 pm3.2 k A F k Z k A F k Z
29 28 necon1bd k A ¬ k A F k Z F k = Z
30 pm3.2 k A G k Z k A G k Z
31 30 necon1bd k A ¬ k A G k Z G k = Z
32 29 31 anim12d k A ¬ k A F k Z ¬ k A G k Z F k = Z G k = Z
33 32 imdistani k A ¬ k A F k Z ¬ k A G k Z k A F k = Z G k = Z
34 15 adantr φ k A F k = Z G k = Z F Fn A
35 20 adantr φ k A F k = Z G k = Z G Fn A
36 1 adantr φ k A F k = Z G k = Z A V
37 simprl φ k A F k = Z G k = Z k A
38 fnfvof F Fn A G Fn A A V k A F X f G k = F k X G k
39 34 35 36 37 38 syl22anc φ k A F k = Z G k = Z F X f G k = F k X G k
40 oveq12 F k = Z G k = Z F k X G k = Z X Z
41 40 ad2antll φ k A F k = Z G k = Z F k X G k = Z X Z
42 5 adantr φ k A F k = Z G k = Z Z X Z = Z
43 39 41 42 3eqtrd φ k A F k = Z G k = Z F X f G k = Z
44 33 43 sylan2 φ k A ¬ k A F k Z ¬ k A G k Z F X f G k = Z
45 27 44 syldan φ k A ¬ k supp Z F ¬ k supp Z G F X f G k = Z
46 14 45 sylan2b φ k A supp Z F supp Z G F X f G k = Z
47 8 46 suppss φ F X f G supp Z supp Z F supp Z G