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 = B A

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 ∈ B A ↔ m : A ⟶ B
9 8 exbiri ⊢ m : A ⟶ B → B ∈ V → m : A ⟶ B → m ∈ B A
10 9 pm2.43b ⊢ B ∈ V → m : A ⟶ B → m ∈ B A
11 elmapi ⊢ m ∈ B A → m : A ⟶ B
12 10 11 impbid1 ⊢ B ∈ V → m : A ⟶ B ↔ m ∈ B A
13 3 12 bitrid ⊢ B ∈ V → m ∈ f | f : A ⟶ B ↔ m ∈ B A
14 13 eqrdv ⊢ B ∈ V → f | f : A ⟶ B = B A