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 φ F V
suppun2.2 φ G W
suppun2.3 φ Z X
Assertion suppun2 φ F G supp Z = supp Z F supp Z G

Proof

Step Hyp Ref Expression
1 suppun2.1 φ F V
2 suppun2.2 φ G W
3 suppun2.3 φ Z X
4 cnvun F G -1 = F -1 G -1
5 4 imaeq1i F G -1 V Z = F -1 G -1 V Z
6 imaundir F -1 G -1 V Z = F -1 V Z G -1 V Z
7 5 6 eqtri F G -1 V Z = F -1 V Z G -1 V Z
8 1 2 unexd φ F G V
9 suppimacnv F G V Z X F G supp Z = F G -1 V Z
10 8 3 9 syl2anc φ F G supp Z = F G -1 V Z
11 suppimacnv F V Z X F supp Z = F -1 V Z
12 1 3 11 syl2anc φ F supp Z = F -1 V Z
13 suppimacnv G W Z X G supp Z = G -1 V Z
14 2 3 13 syl2anc φ G supp Z = G -1 V Z
15 12 14 uneq12d φ supp Z F supp Z G = F -1 V Z G -1 V Z
16 7 10 15 3eqtr4a φ F G supp Z = supp Z F supp Z G