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 𝑍 ) ) )