Metamath Proof Explorer


Theorem frnsuppeq

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 frnsuppeq ( ( 𝐼𝑉𝑍𝑊 ) → ( 𝐹 : 𝐼𝑆 → ( 𝐹 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 𝑍 ) = ( 𝐹 “ ( 𝑆 ∖ { 𝑍 } ) ) ) )