This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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