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	⊢ ( 𝜑 → 𝐺 ∈ 𝑉 )
Assertion	suppun	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) )

Proof

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