Theorem suppun

Description: The support of a class/function is a subset of the support of the union of this class/function with another class/function. (Contributed by AV, 4-Jun-2019)

	Ref	Expression
Hypothesis	suppun.g	|- ( ph -> G e. V )
Assertion	suppun	|- ( ph -> ( F supp Z ) C_ ( ( F u. G ) supp Z ) )

Proof

Step	Hyp	Ref	Expression
1		suppun.g	|- ( ph -> G e. V )
2		ssun1	|- ( `' F " ( _V \ { Z } ) ) C_ ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) )
3		cnvun	|- `' ( F u. G ) = ( `' F u. `' G )
4	3	imaeq1i	|- ( `' ( F u. G ) " ( _V \ { Z } ) ) = ( ( `' F u. `' G ) " ( _V \ { Z } ) )
5		imaundir	|- ( ( `' F u. `' G ) " ( _V \ { Z } ) ) = ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) )
6	4 5	eqtri	|- ( `' ( F u. G ) " ( _V \ { Z } ) ) = ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) )
7	2 6	sseqtrri	|- ( `' F " ( _V \ { Z } ) ) C_ ( `' ( F u. G ) " ( _V \ { Z } ) )
8	7	a1i	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( `' F " ( _V \ { Z } ) ) C_ ( `' ( F u. G ) " ( _V \ { Z } ) ) )
9		suppimacnv	|- ( ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
10	9	adantr	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
11		unexg	|- ( ( F e. _V /\ G e. V ) -> ( F u. G ) e. _V )
12	11	adantlr	|- ( ( ( F e. _V /\ Z e. _V ) /\ G e. V ) -> ( F u. G ) e. _V )
13	1 12	sylan2	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( F u. G ) e. _V )
14		simplr	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> Z e. _V )
15		suppimacnv	|- ( ( ( F u. G ) e. _V /\ Z e. _V ) -> ( ( F u. G ) supp Z ) = ( `' ( F u. G ) " ( _V \ { Z } ) ) )
16	13 14 15	syl2anc	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( ( F u. G ) supp Z ) = ( `' ( F u. G ) " ( _V \ { Z } ) ) )
17	8 10 16	3sstr4d	|- ( ( ( F e. _V /\ Z e. _V ) /\ ph ) -> ( F supp Z ) C_ ( ( F u. G ) supp Z ) )
18	17	ex	|- ( ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ ( ( F u. G ) supp Z ) ) )
19		supp0prc	|- ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) = (/) )
20		0ss	|- (/) C_ ( ( F u. G ) supp Z )
21	19 20	eqsstrdi	|- ( -. ( F e. _V /\ Z e. _V ) -> ( F supp Z ) C_ ( ( F u. G ) supp Z ) )
22	21	a1d	|- ( -. ( F e. _V /\ Z e. _V ) -> ( ph -> ( F supp Z ) C_ ( ( F u. G ) supp Z ) ) )
23	18 22	pm2.61i	|- ( ph -> ( F supp Z ) C_ ( ( F u. G ) supp Z ) )