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 e. Fin /\ A C_ O ) /\ X e. O ) -> ( ( ( _Ind ` O ) ` A ) ` X ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		pr01ssre	|- { 0 , 1 } C_ RR
2		indf	|- ( ( O e. Fin /\ A C_ O ) -> ( ( _Ind ` O ) ` A ) : O --> { 0 , 1 } )
3	2	ffvelcdmda	|- ( ( ( O e. Fin /\ A C_ O ) /\ X e. O ) -> ( ( ( _Ind ` O ) ` A ) ` X ) e. { 0 , 1 } )
4	1 3	sselid	|- ( ( ( O e. Fin /\ A C_ O ) /\ X e. O ) -> ( ( ( _Ind ` O ) ` A ) ` X ) e. RR )