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
|- ( ph -> A e. V )
suppofssd.2
|- ( ph -> Z e. B )
suppofssd.3
|- ( ph -> F : A --> B )
suppofssd.4
|- ( ph -> G : A --> B )
suppofssd.5
|- ( ph -> ( Z X Z ) = Z )
Assertion suppofssd
|- ( ph -> ( ( F oF X G ) supp Z ) C_ ( ( F supp Z ) u. ( G supp Z ) ) )

Proof

Step Hyp Ref Expression
1 suppofssd.1
 |-  ( ph -> A e. V )
2 suppofssd.2
 |-  ( ph -> Z e. B )
3 suppofssd.3
 |-  ( ph -> F : A --> B )
4 suppofssd.4
 |-  ( ph -> G : A --> B )
5 suppofssd.5
 |-  ( ph -> ( Z X Z ) = Z )
6 ovexd
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x X y ) e. _V )
7 inidm
 |-  ( A i^i A ) = A
8 6 3 4 1 1 7 off
 |-  ( ph -> ( F oF X G ) : A --> _V )
9 eldif
 |-  ( k e. ( A \ ( ( F supp Z ) u. ( G supp Z ) ) ) <-> ( k e. A /\ -. k e. ( ( F supp Z ) u. ( G supp Z ) ) ) )
10 ioran
 |-  ( -. ( k e. ( F supp Z ) \/ k e. ( G supp Z ) ) <-> ( -. k e. ( F supp Z ) /\ -. k e. ( G supp Z ) ) )
11 elun
 |-  ( k e. ( ( F supp Z ) u. ( G supp Z ) ) <-> ( k e. ( F supp Z ) \/ k e. ( G supp Z ) ) )
12 10 11 xchnxbir
 |-  ( -. k e. ( ( F supp Z ) u. ( G supp Z ) ) <-> ( -. k e. ( F supp Z ) /\ -. k e. ( G supp Z ) ) )
13 12 anbi2i
 |-  ( ( k e. A /\ -. k e. ( ( F supp Z ) u. ( G supp Z ) ) ) <-> ( k e. A /\ ( -. k e. ( F supp Z ) /\ -. k e. ( G supp Z ) ) ) )
14 9 13 bitri
 |-  ( k e. ( A \ ( ( F supp Z ) u. ( G supp Z ) ) ) <-> ( k e. A /\ ( -. k e. ( F supp Z ) /\ -. k e. ( G supp Z ) ) ) )
15 3 ffnd
 |-  ( ph -> F Fn A )
16 elsuppfn
 |-  ( ( F Fn A /\ A e. V /\ Z e. B ) -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )
17 15 1 2 16 syl3anc
 |-  ( ph -> ( k e. ( F supp Z ) <-> ( k e. A /\ ( F ` k ) =/= Z ) ) )
18 17 notbid
 |-  ( ph -> ( -. k e. ( F supp Z ) <-> -. ( k e. A /\ ( F ` k ) =/= Z ) ) )
19 18 biimpd
 |-  ( ph -> ( -. k e. ( F supp Z ) -> -. ( k e. A /\ ( F ` k ) =/= Z ) ) )
20 4 ffnd
 |-  ( ph -> G Fn A )
21 elsuppfn
 |-  ( ( G Fn A /\ A e. V /\ Z e. B ) -> ( k e. ( G supp Z ) <-> ( k e. A /\ ( G ` k ) =/= Z ) ) )
22 20 1 2 21 syl3anc
 |-  ( ph -> ( k e. ( G supp Z ) <-> ( k e. A /\ ( G ` k ) =/= Z ) ) )
23 22 notbid
 |-  ( ph -> ( -. k e. ( G supp Z ) <-> -. ( k e. A /\ ( G ` k ) =/= Z ) ) )
24 23 biimpd
 |-  ( ph -> ( -. k e. ( G supp Z ) -> -. ( k e. A /\ ( G ` k ) =/= Z ) ) )
25 19 24 anim12d
 |-  ( ph -> ( ( -. k e. ( F supp Z ) /\ -. k e. ( G supp Z ) ) -> ( -. ( k e. A /\ ( F ` k ) =/= Z ) /\ -. ( k e. A /\ ( G ` k ) =/= Z ) ) ) )
26 25 anim2d
 |-  ( ph -> ( ( k e. A /\ ( -. k e. ( F supp Z ) /\ -. k e. ( G supp Z ) ) ) -> ( k e. A /\ ( -. ( k e. A /\ ( F ` k ) =/= Z ) /\ -. ( k e. A /\ ( G ` k ) =/= Z ) ) ) ) )
27 26 imp
 |-  ( ( ph /\ ( k e. A /\ ( -. k e. ( F supp Z ) /\ -. k e. ( G supp Z ) ) ) ) -> ( k e. A /\ ( -. ( k e. A /\ ( F ` k ) =/= Z ) /\ -. ( k e. A /\ ( G ` k ) =/= Z ) ) ) )
28 pm3.2
 |-  ( k e. A -> ( ( F ` k ) =/= Z -> ( k e. A /\ ( F ` k ) =/= Z ) ) )
29 28 necon1bd
 |-  ( k e. A -> ( -. ( k e. A /\ ( F ` k ) =/= Z ) -> ( F ` k ) = Z ) )
30 pm3.2
 |-  ( k e. A -> ( ( G ` k ) =/= Z -> ( k e. A /\ ( G ` k ) =/= Z ) ) )
31 30 necon1bd
 |-  ( k e. A -> ( -. ( k e. A /\ ( G ` k ) =/= Z ) -> ( G ` k ) = Z ) )
32 29 31 anim12d
 |-  ( k e. A -> ( ( -. ( k e. A /\ ( F ` k ) =/= Z ) /\ -. ( k e. A /\ ( G ` k ) =/= Z ) ) -> ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) )
33 32 imdistani
 |-  ( ( k e. A /\ ( -. ( k e. A /\ ( F ` k ) =/= Z ) /\ -. ( k e. A /\ ( G ` k ) =/= Z ) ) ) -> ( k e. A /\ ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) )
34 15 adantr
 |-  ( ( ph /\ ( k e. A /\ ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) ) -> F Fn A )
35 20 adantr
 |-  ( ( ph /\ ( k e. A /\ ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) ) -> G Fn A )
36 1 adantr
 |-  ( ( ph /\ ( k e. A /\ ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) ) -> A e. V )
37 simprl
 |-  ( ( ph /\ ( k e. A /\ ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) ) -> k e. A )
38 fnfvof
 |-  ( ( ( F Fn A /\ G Fn A ) /\ ( A e. V /\ k e. A ) ) -> ( ( F oF X G ) ` k ) = ( ( F ` k ) X ( G ` k ) ) )
39 34 35 36 37 38 syl22anc
 |-  ( ( ph /\ ( k e. A /\ ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) ) -> ( ( F oF X 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
 |-  ( ( ph /\ ( k e. A /\ ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) ) -> ( ( F ` k ) X ( G ` k ) ) = ( Z X Z ) )
42 5 adantr
 |-  ( ( ph /\ ( k e. A /\ ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) ) -> ( Z X Z ) = Z )
43 39 41 42 3eqtrd
 |-  ( ( ph /\ ( k e. A /\ ( ( F ` k ) = Z /\ ( G ` k ) = Z ) ) ) -> ( ( F oF X G ) ` k ) = Z )
44 33 43 sylan2
 |-  ( ( ph /\ ( k e. A /\ ( -. ( k e. A /\ ( F ` k ) =/= Z ) /\ -. ( k e. A /\ ( G ` k ) =/= Z ) ) ) ) -> ( ( F oF X G ) ` k ) = Z )
45 27 44 syldan
 |-  ( ( ph /\ ( k e. A /\ ( -. k e. ( F supp Z ) /\ -. k e. ( G supp Z ) ) ) ) -> ( ( F oF X G ) ` k ) = Z )
46 14 45 sylan2b
 |-  ( ( ph /\ k e. ( A \ ( ( F supp Z ) u. ( G supp Z ) ) ) ) -> ( ( F oF X G ) ` k ) = Z )
47 8 46 suppss
 |-  ( ph -> ( ( F oF X G ) supp Z ) C_ ( ( F supp Z ) u. ( G supp Z ) ) )