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

Metamath Proof Explorer

Theorem fsuppun

Description: The union of two finitely supported functions is finitely supported (but not necessarily a function!). (Contributed by AV, 3-Jun-2019)

Ref Expression
Hypotheses fsuppun.f ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
fsuppun.g ⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
Assertion fsuppun ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 fsuppun.f ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
2 fsuppun.g ⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )
3 cnvun ⊢ ◡ ( 𝐹 ∪ 𝐺 ) = ( ◡ 𝐹 ∪ ◡ 𝐺 )
4 3 imaeq1i ⊢ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 ∪ ◡ 𝐺 ) “ ( V ∖ { 𝑍 } ) )
5 imaundir ⊢ ( ( ◡ 𝐹 ∪ ◡ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
6 4 5 eqtri ⊢ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) = ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
7 unexb ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ↔ ( 𝐹 ∪ 𝐺 ) ∈ V )
8 simpl ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → 𝐹 ∈ V )
9 7 8 sylbir ⊢ ( ( 𝐹 ∪ 𝐺 ) ∈ V → 𝐹 ∈ V )
10 suppimacnv ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
11 9 10 sylan ⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
12 11 eqcomd ⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = ( 𝐹 supp 𝑍 ) )
13 12 adantr ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = ( 𝐹 supp 𝑍 ) )
14 1 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
15 14 adantl ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝐹 supp 𝑍 ) ∈ Fin )
16 13 15 eqeltrd ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
17 simpr ⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → 𝐺 ∈ V )
18 7 17 sylbir ⊢ ( ( 𝐹 ∪ 𝐺 ) ∈ V → 𝐺 ∈ V )
19 suppimacnv ⊢ ( ( 𝐺 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐺 supp 𝑍 ) = ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) )
20 19 eqcomd ⊢ ( ( 𝐺 ∈ V ∧ 𝑍 ∈ V ) → ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) = ( 𝐺 supp 𝑍 ) )
21 18 20 sylan ⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) = ( 𝐺 supp 𝑍 ) )
22 21 adantr ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) = ( 𝐺 supp 𝑍 ) )
23 2 fsuppimpd ⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ∈ Fin )
24 23 adantl ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝐺 supp 𝑍 ) ∈ Fin )
25 22 24 eqeltrd ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
26 unfi ⊢ ( ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∈ Fin ∧ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) ∈ Fin ) → ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
27 16 25 26 syl2anc ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ∪ ( ◡ 𝐺 “ ( V ∖ { 𝑍 } ) ) ) ∈ Fin )
28 6 27 eqeltrid ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ∈ Fin )
29 suppimacnv ⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) = ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) )
30 29 eleq1d ⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ↔ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ∈ Fin ) )
31 30 adantr ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ↔ ( ◡ ( 𝐹 ∪ 𝐺 ) “ ( V ∖ { 𝑍 } ) ) ∈ Fin ) )
32 28 31 mpbird ⊢ ( ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )
33 32 ex ⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) )
34 supp0prc ⊢ ( ¬ ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) = ∅ )
35 0fi ⊢ ∅ ∈ Fin
36 34 35 eqeltrdi ⊢ ( ¬ ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )
37 36 a1d ⊢ ( ¬ ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) )
38 33 37 pm2.61i ⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin )