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

Metamath Proof Explorer

Theorem indsn

Description: The indicator function of a singleton. (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Assertion indsn ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ { 𝑋 } ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → 𝑋 ∈ 𝑂 )
2 1 snssd ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → { 𝑋 } ⊆ 𝑂 )
3 indval ⊢ ( ( 𝑂 ∈ 𝑉 ∧ { 𝑋 } ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ { 𝑋 } ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ { 𝑋 } , 1 , 0 ) ) )
4 2 3 syldan ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ { 𝑋 } ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ { 𝑋 } , 1 , 0 ) ) )
5 velsn ⊢ ( 𝑥 ∈ { 𝑋 } ↔ 𝑥 = 𝑋 )
6 5 a1i ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( 𝑥 ∈ { 𝑋 } ↔ 𝑥 = 𝑋 ) )
7 6 ifbid ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → if ( 𝑥 ∈ { 𝑋 } , 1 , 0 ) = if ( 𝑥 = 𝑋 , 1 , 0 ) )
8 7 mpteq2dv ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ { 𝑋 } , 1 , 0 ) ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) ) )
9 4 8 eqtrd ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑋 ∈ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ { 𝑋 } ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 = 𝑋 , 1 , 0 ) ) )