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 ⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
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 𝑍 ) ) )