Theorem mptelee

Description: A condition for a mapping to be an element of a Euclidean space. (Contributed by Scott Fenton, 7-Jun-2013) (Proof shortened by SN, 2-Feb-2026)

	Ref	Expression
Assertion	mptelee	|- ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( A F B ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( A F B ) e. RR ) )

Proof

Step	Hyp	Ref	Expression
1		elee	|- ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( A F B ) ) e. ( EE ` N ) <-> ( k e. ( 1 ... N ) |-> ( A F B ) ) : ( 1 ... N ) --> RR ) )
2		eqid	|- ( k e. ( 1 ... N ) |-> ( A F B ) ) = ( k e. ( 1 ... N ) |-> ( A F B ) )
3	2	fmpt	|- ( A. k e. ( 1 ... N ) ( A F B ) e. RR <-> ( k e. ( 1 ... N ) |-> ( A F B ) ) : ( 1 ... N ) --> RR )
4	1 3	bitr4di	|- ( N e. NN -> ( ( k e. ( 1 ... N ) |-> ( A F B ) ) e. ( EE ` N ) <-> A. k e. ( 1 ... N ) ( A F B ) e. RR ) )