Theorem frnsuppeqg

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

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

Proof

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