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

Metamath Proof Explorer

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