Theorem fvindre

Description: The range of the indicator function is a subset of RR . (Contributed by AV, 10-Apr-2026)

	Ref	Expression
Assertion	fvindre	⊢ ( ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑋 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		pr01ssre	⊢ { 0 , 1 } ⊆ ℝ
2		indf	⊢ ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) → ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) : 𝑂 ⟶ { 0 , 1 } )
3	2	ffvelcdmda	⊢ ( ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑋 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) ∈ { 0 , 1 } )
4	1 3	sselid	⊢ ( ( ( 𝑂 ∈ Fin ∧ 𝐴 ⊆ 𝑂 ) ∧ 𝑋 ∈ 𝑂 ) → ( ( ( 𝟭 ‘ 𝑂 ) ‘ 𝐴 ) ‘ 𝑋 ) ∈ ℝ )