This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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