Metamath Proof Explorer

Theorem suppun

Description: The support of a class/function is a subset of the support of the union of this class/function with another class/function. (Contributed by AV, 4-Jun-2019)

Ref Expression
Hypothesis suppun.g ⊢ φ → G ∈ V
Assertion suppun ⊢ φ → F supp Z ⊆ F ∪ G supp Z

Proof

Step Hyp Ref Expression
1 suppun.g ⊢ φ → G ∈ V
2 ssun1 ⊢ F -1 V ∖ Z ⊆ F -1 V ∖ Z ∪ G -1 V ∖ Z
3 cnvun ⊢ F ∪ G -1 = F -1 ∪ G -1
4 3 imaeq1i ⊢ F ∪ G -1 V ∖ Z = F -1 ∪ G -1 V ∖ Z
5 imaundir ⊢ F -1 ∪ G -1 V ∖ Z = F -1 V ∖ Z ∪ G -1 V ∖ Z
6 4 5 eqtri ⊢ F ∪ G -1 V ∖ Z = F -1 V ∖ Z ∪ G -1 V ∖ Z
7 2 6 sseqtrri ⊢ F -1 V ∖ Z ⊆ F ∪ G -1 V ∖ Z
8 7 a1i ⊢ F ∈ V ∧ Z ∈ V ∧ φ → F -1 V ∖ Z ⊆ F ∪ G -1 V ∖ Z
9 suppimacnv ⊢ F ∈ V ∧ Z ∈ V → F supp Z = F -1 V ∖ Z
10 9 adantr ⊢ F ∈ V ∧ Z ∈ V ∧ φ → F supp Z = F -1 V ∖ Z
11 unexg ⊢ F ∈ V ∧ G ∈ V → F ∪ G ∈ V
12 11 adantlr ⊢ F ∈ V ∧ Z ∈ V ∧ G ∈ V → F ∪ G ∈ V
13 1 12 sylan2 ⊢ F ∈ V ∧ Z ∈ V ∧ φ → F ∪ G ∈ V
14 simplr ⊢ F ∈ V ∧ Z ∈ V ∧ φ → Z ∈ V
15 suppimacnv ⊢ F ∪ G ∈ V ∧ Z ∈ V → F ∪ G supp Z = F ∪ G -1 V ∖ Z
16 13 14 15 syl2anc ⊢ F ∈ V ∧ Z ∈ V ∧ φ → F ∪ G supp Z = F ∪ G -1 V ∖ Z
17 8 10 16 3sstr4d ⊢ F ∈ V ∧ Z ∈ V ∧ φ → F supp Z ⊆ F ∪ G supp Z
18 17 ex ⊢ F ∈ V ∧ Z ∈ V → φ → F supp Z ⊆ F ∪ G supp Z
19 supp0prc ⊢ ¬ F ∈ V ∧ Z ∈ V → F supp Z = ∅
20 0ss ⊢ ∅ ⊆ F ∪ G supp Z
21 19 20 eqsstrdi ⊢ ¬ F ∈ V ∧ Z ∈ V → F supp Z ⊆ F ∪ G supp Z
22 21 a1d ⊢ ¬ F ∈ V ∧ Z ∈ V → φ → F supp Z ⊆ F ∪ G supp Z
23 18 22 pm2.61i ⊢ φ → F supp Z ⊆ F ∪ G supp Z