Theorem suppun2

Description: The support of a union is the union of the supports. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	suppun2.1	|- ( ph -> F e. V )
	suppun2.2	|- ( ph -> G e. W )
	suppun2.3	|- ( ph -> Z e. X )
Assertion	suppun2	|- ( ph -> ( ( F u. G ) supp Z ) = ( ( F supp Z ) u. ( G supp Z ) ) )

Proof

Step	Hyp	Ref	Expression
1		suppun2.1	|- ( ph -> F e. V )
2		suppun2.2	|- ( ph -> G e. W )
3		suppun2.3	|- ( ph -> Z e. X )
4		cnvun	|- `' ( F u. G ) = ( `' F u. `' G )
5	4	imaeq1i	|- ( `' ( F u. G ) " ( _V \ { Z } ) ) = ( ( `' F u. `' G ) " ( _V \ { Z } ) )
6		imaundir	|- ( ( `' F u. `' G ) " ( _V \ { Z } ) ) = ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) )
7	5 6	eqtri	|- ( `' ( F u. G ) " ( _V \ { Z } ) ) = ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) )
8	1 2	unexd	|- ( ph -> ( F u. G ) e. _V )
9		suppimacnv	|- ( ( ( F u. G ) e. _V /\ Z e. X ) -> ( ( F u. G ) supp Z ) = ( `' ( F u. G ) " ( _V \ { Z } ) ) )
10	8 3 9	syl2anc	|- ( ph -> ( ( F u. G ) supp Z ) = ( `' ( F u. G ) " ( _V \ { Z } ) ) )
11		suppimacnv	|- ( ( F e. V /\ Z e. X ) -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
12	1 3 11	syl2anc	|- ( ph -> ( F supp Z ) = ( `' F " ( _V \ { Z } ) ) )
13		suppimacnv	|- ( ( G e. W /\ Z e. X ) -> ( G supp Z ) = ( `' G " ( _V \ { Z } ) ) )
14	2 3 13	syl2anc	|- ( ph -> ( G supp Z ) = ( `' G " ( _V \ { Z } ) ) )
15	12 14	uneq12d	|- ( ph -> ( ( F supp Z ) u. ( G supp Z ) ) = ( ( `' F " ( _V \ { Z } ) ) u. ( `' G " ( _V \ { Z } ) ) ) )
16	7 10 15	3eqtr4a	|- ( ph -> ( ( F u. G ) supp Z ) = ( ( F supp Z ) u. ( G supp Z ) ) )