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

Metamath Proof Explorer

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 ) ) )