Theorem mapfset

Description: If B is a set, the value of the set exponentiation ( B ^m A ) is the class of all functions from A to B . Generalisation of mapvalg (which does not require ax-rep ) to arbitrary domains. Note that the class { f | f : A --> B } can only contain set-functions, as opposed to arbitrary class-functions. When A is a proper class, there can be no set-functions on it, so the above class is empty (see also fsetdmprc0 ), hence a set. In this case, both sides of the equality in this theorem are the empty set. (Contributed by AV, 8-Aug-2024)

	Ref	Expression
Assertion	mapfset	|- ( B e. V -> { f | f : A --> B } = ( B ^m A ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- m e. _V
2		feq1	|- ( f = m -> ( f : A --> B <-> m : A --> B ) )
3	1 2	elab	|- ( m e. { f | f : A --> B } <-> m : A --> B )
4		simpr	|- ( ( m : A --> B /\ B e. V ) -> B e. V )
5		dmfex	|- ( ( m e. _V /\ m : A --> B ) -> A e. _V )
6	1 5	mpan	|- ( m : A --> B -> A e. _V )
7	6	adantr	|- ( ( m : A --> B /\ B e. V ) -> A e. _V )
8	4 7	elmapd	|- ( ( m : A --> B /\ B e. V ) -> ( m e. ( B ^m A ) <-> m : A --> B ) )
9	8	exbiri	|- ( m : A --> B -> ( B e. V -> ( m : A --> B -> m e. ( B ^m A ) ) ) )
10	9	pm2.43b	|- ( B e. V -> ( m : A --> B -> m e. ( B ^m A ) ) )
11		elmapi	|- ( m e. ( B ^m A ) -> m : A --> B )
12	10 11	impbid1	|- ( B e. V -> ( m : A --> B <-> m e. ( B ^m A ) ) )
13	3 12	bitrid	|- ( B e. V -> ( m e. { f | f : A --> B } <-> m e. ( B ^m A ) ) )
14	13	eqrdv	|- ( B e. V -> { f | f : A --> B } = ( B ^m A ) )