Metamath Proof Explorer

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∈V→f|f:A⟶B=BA

Proof

Step Hyp Ref Expression
1 vex ⊢m∈V
2 feq1 ⊢f=m→f:A⟶B↔m:A⟶B
3 1 2 elab ⊢m∈f|f:A⟶B↔m:A⟶B
4 simpr ⊢m:A⟶B∧B∈V→B∈V
5 dmfex ⊢m∈V∧m:A⟶B→A∈V
6 1 5 mpan ⊢m:A⟶B→A∈V
7 6 adantr ⊢m:A⟶B∧B∈V→A∈V
8 4 7 elmapd ⊢m:A⟶B∧B∈V→m∈BA↔m:A⟶B
9 8 exbiri ⊢m:A⟶B→B∈V→m:A⟶B→m∈BA
10 9 pm2.43b ⊢B∈V→m:A⟶B→m∈BA
11 elmapi ⊢m∈BA→m:A⟶B
12 10 11 impbid1 ⊢B∈V→m:A⟶B↔m∈BA
13 3 12 bitrid ⊢B∈V→m∈f|f:A⟶B↔m∈BA
14 13 eqrdv ⊢B∈V→f|f:A⟶B=BA