Metamath Proof Explorer

Theorem indsupp

Description: The support of the indicator function. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Assertion indsupp ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A supp 0 = A

Proof

Step Hyp Ref Expression
1 simpl ⊢ O ∈ V ∧ A ⊆ O → O ∈ V
2 c0ex ⊢ 0 ∈ V
3 2 a1i ⊢ O ∈ V ∧ A ⊆ O → 0 ∈ V
4 indf ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A : O ⟶ 0 1
5 fsuppeq ⊢ O ∈ V ∧ 0 ∈ V → 𝟙 O ⁡ A : O ⟶ 0 1 → 𝟙 O ⁡ A supp 0 = 𝟙 O ⁡ A -1 0 1 ∖ 0
6 5 imp ⊢ O ∈ V ∧ 0 ∈ V ∧ 𝟙 O ⁡ A : O ⟶ 0 1 → 𝟙 O ⁡ A supp 0 = 𝟙 O ⁡ A -1 0 1 ∖ 0
7 1 3 4 6 syl21anc ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A supp 0 = 𝟙 O ⁡ A -1 0 1 ∖ 0
8 prcom ⊢ 0 1 = 1 0
9 8 difeq1i ⊢ 0 1 ∖ 0 = 1 0 ∖ 0
10 ax-1ne0 ⊢ 1 ≠ 0
11 difprsn2 ⊢ 1 ≠ 0 → 1 0 ∖ 0 = 1
12 10 11 ax-mp ⊢ 1 0 ∖ 0 = 1
13 9 12 eqtri ⊢ 0 1 ∖ 0 = 1
14 13 a1i ⊢ O ∈ V ∧ A ⊆ O → 0 1 ∖ 0 = 1
15 14 imaeq2d ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A -1 0 1 ∖ 0 = 𝟙 O ⁡ A -1 1
16 indpi1 ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A -1 1 = A
17 7 15 16 3eqtrd ⊢ O ∈ V ∧ A ⊆ O → 𝟙 O ⁡ A supp 0 = A