Metamath Proof Explorer

Theorem suppofss2d

Description: Condition for the support of a function operation to be a subset of the support of the right function term. (Contributed by Thierry Arnoux, 21-Jun-2019)

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 )
suppofss2d.5 
|- ( ( ph /\ x e. B ) -> ( x X Z ) = Z )
Assertion suppofss2d 
|- ( ph -> ( ( F oF X G ) supp Z ) C_ ( 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 suppofss2d.5 
 |-  ( ( ph /\ x e. B ) -> ( x X Z ) = Z )
6 3 ffnd 
 |-  ( ph -> F Fn A )
7 4 ffnd 
 |-  ( ph -> G Fn A )
8 inidm 
 |-  ( A i^i A ) = A
9 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) = ( F ` y ) )
10 eqidd 
 |-  ( ( ph /\ y e. A ) -> ( G ` y ) = ( G ` y ) )
11 6 7 1 1 8 9 10 ofval 
 |-  ( ( ph /\ y e. A ) -> ( ( F oF X G ) ` y ) = ( ( F ` y ) X ( G ` y ) ) )
12 11 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ ( G ` y ) = Z ) -> ( ( F oF X G ) ` y ) = ( ( F ` y ) X ( G ` y ) ) )
13 simpr 
 |-  ( ( ( ph /\ y e. A ) /\ ( G ` y ) = Z ) -> ( G ` y ) = Z )
14 13 oveq2d 
 |-  ( ( ( ph /\ y e. A ) /\ ( G ` y ) = Z ) -> ( ( F ` y ) X ( G ` y ) ) = ( ( F ` y ) X Z ) )
15 5 ralrimiva 
 |-  ( ph -> A. x e. B ( x X Z ) = Z )
16 15 adantr 
 |-  ( ( ph /\ y e. A ) -> A. x e. B ( x X Z ) = Z )
17 3 ffvelrnda 
 |-  ( ( ph /\ y e. A ) -> ( F ` y ) e. B )
18 simpr 
 |-  ( ( ( ph /\ y e. A ) /\ x = ( F ` y ) ) -> x = ( F ` y ) )
19 18 oveq1d 
 |-  ( ( ( ph /\ y e. A ) /\ x = ( F ` y ) ) -> ( x X Z ) = ( ( F ` y ) X Z ) )
20 19 eqeq1d 
 |-  ( ( ( ph /\ y e. A ) /\ x = ( F ` y ) ) -> ( ( x X Z ) = Z <-> ( ( F ` y ) X Z ) = Z ) )
21 17 20 rspcdv 
 |-  ( ( ph /\ y e. A ) -> ( A. x e. B ( x X Z ) = Z -> ( ( F ` y ) X Z ) = Z ) )
22 16 21 mpd 
 |-  ( ( ph /\ y e. A ) -> ( ( F ` y ) X Z ) = Z )
23 22 adantr 
 |-  ( ( ( ph /\ y e. A ) /\ ( G ` y ) = Z ) -> ( ( F ` y ) X Z ) = Z )
24 12 14 23 3eqtrd 
 |-  ( ( ( ph /\ y e. A ) /\ ( G ` y ) = Z ) -> ( ( F oF X G ) ` y ) = Z )
25 24 ex 
 |-  ( ( ph /\ y e. A ) -> ( ( G ` y ) = Z -> ( ( F oF X G ) ` y ) = Z ) )
26 25 ralrimiva 
 |-  ( ph -> A. y e. A ( ( G ` y ) = Z -> ( ( F oF X G ) ` y ) = Z ) )
27 6 7 1 1 8 offn 
 |-  ( ph -> ( F oF X G ) Fn A )
28 ssidd 
 |-  ( ph -> A C_ A )
29 suppfnss 
 |-  ( ( ( ( F oF X G ) Fn A /\ G Fn A ) /\ ( A C_ A /\ A e. V /\ Z e. B ) ) -> ( A. y e. A ( ( G ` y ) = Z -> ( ( F oF X G ) ` y ) = Z ) -> ( ( F oF X G ) supp Z ) C_ ( G supp Z ) ) )
30 27 7 28 1 2 29 syl23anc 
 |-  ( ph -> ( A. y e. A ( ( G ` y ) = Z -> ( ( F oF X G ) ` y ) = Z ) -> ( ( F oF X G ) supp Z ) C_ ( G supp Z ) ) )
31 26 30 mpd 
 |-  ( ph -> ( ( F oF X G ) supp Z ) C_ ( G supp Z ) )