Theorem suppiniseg

Description: Relation between the support ( F supp Z ) and the initial segment (`' F " { Z } ) ` . (Contributed by Thierry Arnoux, 25-Jun-2024)

	Ref	Expression
Assertion	suppiniseg	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) = ( ◡ 𝐹 “ { 𝑍 } ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	⊢ ( 𝑥 ∈ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) )
2		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
3	2	biimpi	⊢ ( Fun 𝐹 → 𝐹 Fn dom 𝐹 )
4		elsuppfng	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) ) )
5	3 4	syl3an1	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) ) )
6	5	baibd	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
7	6	notbid	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ) )
8		nne	⊢ ( ¬ ( 𝐹 ‘ 𝑥 ) ≠ 𝑍 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑍 )
9	7 8	bitrdi	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
10		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
11	10	elsn	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ↔ ( 𝐹 ‘ 𝑥 ) = 𝑍 )
12	9 11	bitr4di	⊢ ( ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) )
13	12	pm5.32da	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( ( 𝑥 ∈ dom 𝐹 ∧ ¬ 𝑥 ∈ ( 𝐹 supp 𝑍 ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) ) )
14	1 13	syl5bb	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) ) )
15	3	3ad2ant1	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝐹 Fn dom 𝐹 )
16		elpreima	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑍 } ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) ) )
17	15 16	syl	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝑍 } ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 𝑍 } ) ) )
18	14 17	bitr4d	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑥 ∈ ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) ↔ 𝑥 ∈ ( ◡ 𝐹 “ { 𝑍 } ) ) )
19	18	eqrdv	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( dom 𝐹 ∖ ( 𝐹 supp 𝑍 ) ) = ( ◡ 𝐹 “ { 𝑍 } ) )