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

Metamath Proof Explorer

Theorem fsuppeqg

Description: Version of fsuppeq avoiding ax-rep by assuming F is a set rather than its domain I . (Contributed by SN, 30-Jul-2024)

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

Proof

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