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

Metamath Proof Explorer

Theorem fsuppeq

Description: Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Assertion fsuppeq ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) )

Proof

Step Hyp Ref Expression
1 fex ⊢ ( ( 𝐹 : 𝐼 ⟶ 𝑆 ∧ 𝐼 ∈ 𝑉 ) → 𝐹 ∈ V )
2 1 expcom ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 : 𝐼 ⟶ 𝑆 → 𝐹 ∈ V ) )
3 2 adantr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → 𝐹 ∈ V ) )
4 3 imp ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → 𝐹 ∈ V )
5 simplr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → 𝑍 ∈ 𝑊 )
6 suppimacnv ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
7 4 5 6 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
8 ffun ⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → Fun 𝐹 )
9 inpreima ⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) ) = ( ( ◡ 𝐹 “ 𝑆 ) ∩ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
10 8 9 syl ⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) ) = ( ( ◡ 𝐹 “ 𝑆 ) ∩ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) )
11 cnvimass ⊢ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ dom 𝐹
12 fdm ⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → dom 𝐹 = 𝐼 )
13 fimacnv ⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ 𝑆 ) = 𝐼 )
14 12 13 eqtr4d ⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → dom 𝐹 = ( ◡ 𝐹 “ 𝑆 ) )
15 11 14 sseqtrid ⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ ( ◡ 𝐹 “ 𝑆 ) )
16 sseqin2 ⊢ ( ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ⊆ ( ◡ 𝐹 “ 𝑆 ) ↔ ( ( ◡ 𝐹 “ 𝑆 ) ∩ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
17 15 16 sylib ⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ( ◡ 𝐹 “ 𝑆 ) ∩ ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
18 10 17 eqtrd ⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) ) = ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) )
19 invdif ⊢ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) = ( 𝑆 ∖ { 𝑍 } )
20 19 imaeq2i ⊢ ( ◡ 𝐹 “ ( 𝑆 ∩ ( V ∖ { 𝑍 } ) ) ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) )
21 18 20 eqtr3di ⊢ ( 𝐹 : 𝐼 ⟶ 𝑆 → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) )
22 21 adantl ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( ◡ 𝐹 “ ( V ∖ { 𝑍 } ) ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) )
23 7 22 eqtrd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝐹 : 𝐼 ⟶ 𝑆 ) → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) )
24 23 ex ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝐹 : 𝐼 ⟶ 𝑆 → ( 𝐹 supp 𝑍 ) = ( ◡ 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) )