Metamath Proof Explorer

Theorem fvindre

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

Ref Expression
Assertion fvindre ⊢ O ∈ Fin ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X ∈ ℝ

Proof

Step Hyp Ref Expression
1 pr01ssre ⊢ 0 1 ⊆ ℝ
2 indf ⊢ O ∈ Fin ∧ A ⊆ O → 𝟙 O ⁡ A : O ⟶ 0 1
3 2 ffvelcdmda ⊢ O ∈ Fin ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X ∈ 0 1
4 1 3 sselid ⊢ O ∈ Fin ∧ A ⊆ O ∧ X ∈ O → 𝟙 O ⁡ A ⁡ X ∈ ℝ