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	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	suppun2.2	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	suppun2.3	⊢ ( 𝜑 → 𝑍 ∈ 𝑋 )
Assertion	suppun2	⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) = ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		suppun2.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		suppun2.2	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
3		suppun2.3	⊢ ( 𝜑 → 𝑍 ∈ 𝑋 )
4		cnvun	⊢ ◡ ( 𝐹 ∪ 𝐺 ) = ( ◡ 𝐹 ∪ ◡ 𝐺 )
5	4	imaeq1i	⊢ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 ∪ ◡ 𝐺 ) “ ( V ∖ { 𝑍 } ) )
6		imaundir	⊢ ( ( ◡ 𝐹 ∪ ◡ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
7	5 6	eqtri	⊢ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
8	1 2	unexd	⊢ ( 𝜑 → ( 𝐹 ∪ 𝐺 ) ∈ V )
9		suppimacnv	⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ 𝑋 ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) = ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) )
10	8 3 9	syl2anc	⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) = ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) )
11		suppimacnv	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑋 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
12	1 3 11	syl2anc	⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
13		suppimacnv	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑍 ∈ 𝑋 ) → ( 𝐺 supp 𝑍 ) = ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
14	2 3 13	syl2anc	⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) = ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
15	12 14	uneq12d	⊢ ( 𝜑 → ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) = ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) ) )
16	7 10 15	3eqtr4a	⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) = ( ( 𝐹 supp 𝑍 ) ∪ ( 𝐺 supp 𝑍 ) ) )