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