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 ⊢φ→FsuppZ⊆F∪GsuppZ

Proof

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