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 ⊢ φ → O ∈ V
indfsid.2 ⊢ φ → F : O ⟶ 0 1
Assertion indfsid ⊢ φ → F = 𝟙 O ⁡ F supp 0

Proof

Step Hyp Ref Expression
1 indfsid.1 ⊢ φ → O ∈ V
2 indfsid.2 ⊢ φ → F : O ⟶ 0 1
3 indpreima ⊢ O ∈ V ∧ F : O ⟶ 0 1 → F = 𝟙 O ⁡ F -1 1
4 1 2 3 syl2anc ⊢ φ → F = 𝟙 O ⁡ F -1 1
5 c0ex ⊢ 0 ∈ V
6 5 a1i ⊢ φ → 0 ∈ V
7 fsuppeq ⊢ O ∈ V ∧ 0 ∈ V → F : O ⟶ 0 1 → F supp 0 = F -1 0 1 ∖ 0
8 7 imp ⊢ O ∈ V ∧ 0 ∈ V ∧ F : O ⟶ 0 1 → F supp 0 = F -1 0 1 ∖ 0
9 1 6 2 8 syl21anc ⊢ φ → F supp 0 = F -1 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 ⊢ φ → F -1 0 1 ∖ 0 = F -1 1
14 9 13 eqtrd ⊢ φ → F supp 0 = F -1 1
15 14 fveq2d ⊢ φ → 𝟙 O ⁡ F supp 0 = 𝟙 O ⁡ F -1 1
16 4 15 eqtr4d ⊢ φ → F = 𝟙 O ⁡ F supp 0