Theorem indf

Description: An indicator function as a function with domain and codomain. (Contributed by Thierry Arnoux, 13-Aug-2017)

	Ref	Expression
Assertion	indf	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		indval	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) = ( 𝑥 ∈ 𝑂 ↦ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ) )
2		1re	⊢ 1 ∈ ℝ
3		0re	⊢ 0 ∈ ℝ
4		ifpr	⊢ ( ( 1 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 1 , 0 } )
5	2 3 4	mp2an	⊢ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 1 , 0 }
6		prcom	⊢ { 1 , 0 } = { 0 , 1 }
7	5 6	eleqtri	⊢ if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 }
8	7	a1i	⊢ ( ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑥 ∈ 𝑂 ) → if ( 𝑥 ∈ 𝐴 , 1 , 0 ) ∈ { 0 , 1 } )
9	1 8	fmpt3d	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )