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	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = ( 𝐵 ↑m 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑚 ∈ V
2		feq1	⊢ ( 𝑓 = 𝑚 → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ 𝑚 : 𝐴 ⟶ 𝐵 ) )
3	1 2	elab	⊢ ( 𝑚 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↔ 𝑚 : 𝐴 ⟶ 𝐵 )
4		simpr	⊢ ( ( 𝑚 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
5		dmfex	⊢ ( ( 𝑚 ∈ V ∧ 𝑚 : 𝐴 ⟶ 𝐵 ) → 𝐴 ∈ V )
6	1 5	mpan	⊢ ( 𝑚 : 𝐴 ⟶ 𝐵 → 𝐴 ∈ V )
7	6	adantr	⊢ ( ( 𝑚 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V )
8	4 7	elmapd	⊢ ( ( 𝑚 : 𝐴 ⟶ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑚 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝑚 : 𝐴 ⟶ 𝐵 ) )
9	8	exbiri	⊢ ( 𝑚 : 𝐴 ⟶ 𝐵 → ( 𝐵 ∈ 𝑉 → ( 𝑚 : 𝐴 ⟶ 𝐵 → 𝑚 ∈ ( 𝐵 ↑m 𝐴 ) ) ) )
10	9	pm2.43b	⊢ ( 𝐵 ∈ 𝑉 → ( 𝑚 : 𝐴 ⟶ 𝐵 → 𝑚 ∈ ( 𝐵 ↑m 𝐴 ) ) )
11		elmapi	⊢ ( 𝑚 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑚 : 𝐴 ⟶ 𝐵 )
12	10 11	impbid1	⊢ ( 𝐵 ∈ 𝑉 → ( 𝑚 : 𝐴 ⟶ 𝐵 ↔ 𝑚 ∈ ( 𝐵 ↑m 𝐴 ) ) )
13	3 12	syl5bb	⊢ ( 𝐵 ∈ 𝑉 → ( 𝑚 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↔ 𝑚 ∈ ( 𝐵 ↑m 𝐴 ) ) )
14	13	eqrdv	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = ( 𝐵 ↑m 𝐴 ) )