Theorem indfsid

Description: Conditions for a function to be an indicator function. (Contributed by Thierry Arnoux, 18-Jan-2026)

	Ref	Expression
Hypotheses	indfsid.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
	indfsid.2	⊢ ( 𝜑 → 𝐹 : 𝑂 ⟶ { 0 , 1 } )
Assertion	indfsid	⊢ ( 𝜑 → 𝐹 = ( ( 𝟭 ‘ 𝑂 ) ‘ ( 𝐹 supp 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		indfsid.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
2		indfsid.2	⊢ ( 𝜑 → 𝐹 : 𝑂 ⟶ { 0 , 1 } )
3		indpreima	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → 𝐹 = ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → 𝐹 = ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) )
5		c0ex	⊢ 0 ∈ V
6	5	a1i	⊢ ( 𝜑 → 0 ∈ V )
7		fsuppeq	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝐹 : 𝑂 ⟶ { 0 , 1 } → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( { 0 , 1 } ∖ { 0 } ) ) ) )
8	7	imp	⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 0 ∈ V ) ∧ 𝐹 : 𝑂 ⟶ { 0 , 1 } ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( { 0 , 1 } ∖ { 0 } ) ) )
9	1 6 2 8	syl21anc	⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ( { 0 , 1 } ∖ { 0 } ) ) )
10		0ne1	⊢ 0 ≠ 1
11		difprsn1	⊢ ( 0 ≠ 1 → ( { 0 , 1 } ∖ { 0 } ) = { 1 } )
12	10 11	mp1i	⊢ ( 𝜑 → ( { 0 , 1 } ∖ { 0 } ) = { 1 } )
13	12	imaeq2d	⊢ ( 𝜑 → ( ◡ 𝐹 “ ( { 0 , 1 } ∖ { 0 } ) ) = ( ◡ 𝐹 “ { 1 } ) )
14	9 13	eqtrd	⊢ ( 𝜑 → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ { 1 } ) )
15	14	fveq2d	⊢ ( 𝜑 → ( ( 𝟭 ‘ 𝑂 ) ‘ ( 𝐹 supp 0 ) ) = ( ( 𝟭 ‘ 𝑂 ) ‘ ( ◡ 𝐹 “ { 1 } ) ) )
16	4 15	eqtr4d	⊢ ( 𝜑 → 𝐹 = ( ( 𝟭 ‘ 𝑂 ) ‘ ( 𝐹 supp 0 ) ) )