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 
|- ( 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 ) ) )