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

Metamath Proof Explorer

Theorem indfval

Description: Value of the indicator function. (Contributed by Thierry Arnoux, 13-Aug-2017)

Ref Expression
Assertion indfval ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 indval ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )
2 1 3adant3 ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )
3 simpr ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
4 3 eleq1d ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) ∧ 𝑥 = 𝑋 ) → ( 𝑥 ∈ 𝐴 ↔ 𝑋 ∈ 𝐴 ) )
5 4 ifbid ⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) ∧ 𝑥 = 𝑋 ) → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) )
6 simp3 ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → 𝑋 ∈ 𝑂 )
7 1re ⊢ 1 ∈ ℝ
8 0re ⊢ 0 ∈ ℝ
9 7 8 ifcli ⊢ if ( 𝑋 ∈ 𝐴 , 1 , 0 ) ∈ ℝ
10 9 a1i ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → if ( 𝑋 ∈ 𝐴 , 1 , 0 ) ∈ ℝ )
11 2 5 6 10 fvmptd ⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ∧ 𝑋 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) = if ( 𝑋 ∈ 𝐴 , 1 , 0 ) )