Theorem indsupp

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

	Ref	Expression
Assertion	indsupp	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 𝑂 ∈ 𝑉 )
2		c0ex	⊢ 0 ∈ V
3	2	a1i	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → 0 ∈ V )
4		indf	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
5		fsuppeq	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 0 ∈ V ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) = ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ ( { 0 , 1 } ∖ { 0 } ) ) ) )
6	5	imp	⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 0 ∈ V ) ∧ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) = ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ ( { 0 , 1 } ∖ { 0 } ) ) )
7	1 3 4 6	syl21anc	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) = ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ ( { 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	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( { 0 , 1 } ∖ { 0 } ) = { 1 } )
15	14	imaeq2d	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ ( { 0 , 1 } ∖ { 0 } ) ) = ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) )
16		indpi1	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ◡ ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) “ { 1 } ) = 𝐴 )
17	7 15 16	3eqtrd	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) supp 0 ) = 𝐴 )