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 ⊢ φ → 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