Metamath Proof Explorer

Theorem mapvalg

Description: The value of set exponentiation. ( A ^m B ) is the set of all functions that map from B to A . Definition 10.24 of Kunen p. 24. (Contributed by NM, 8-Dec-2003) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	mapvalg	$⊢ (A \in C \land B \in D) \to A^{B} = \{f \| f : B ⟶ A\}$

Proof

Step	Hyp	Ref	Expression
1		mapex	$⊢ (B \in D \land A \in C) \to \{f \| f : B ⟶ A\} \in V$
2	1	ancoms	$⊢ (A \in C \land B \in D) \to \{f \| f : B ⟶ A\} \in V$
3		elex	$⊢ A \in C \to A \in V$
4		elex	$⊢ B \in D \to B \in V$
5		feq3	$⊢ x = A \to (f : y ⟶ x \leftrightarrow f : y ⟶ A)$
6	5	abbidv	$⊢ x = A \to \{f \| f : y ⟶ x\} = \{f \| f : y ⟶ A\}$
7		feq2	$⊢ y = B \to (f : y ⟶ A \leftrightarrow f : B ⟶ A)$
8	7	abbidv	$⊢ y = B \to \{f \| f : y ⟶ A\} = \{f \| f : B ⟶ A\}$
9		df-map	$⊢ ↑_{𝑚} = (x \in V, y \in V ⟼ \{f \| f : y ⟶ x\})$
10	6 8 9	ovmpog	$⊢ (A \in V \land B \in V \land \{f \| f : B ⟶ A\} \in V) \to A^{B} = \{f \| f : B ⟶ A\}$
11	10	3expia	$⊢ (A \in V \land B \in V) \to (\{f \| f : B ⟶ A\} \in V \to A^{B} = \{f \| f : B ⟶ A\})$
12	3 4 11	syl2an	$⊢ (A \in C \land B \in D) \to (\{f \| f : B ⟶ A\} \in V \to A^{B} = \{f \| f : B ⟶ A\})$
13	2 12	mpd	$⊢ (A \in C \land B \in D) \to A^{B} = \{f \| f : B ⟶ A\}$