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

Proof

Step	Hyp	Ref	Expression
1		mapex	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝐴 ∈ 𝐶 ) → { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } ∈ V )
2	1	ancoms	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } ∈ V )
3		elex	⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V )
4		elex	⊢ ( 𝐵 ∈ 𝐷 → 𝐵 ∈ V )
5		feq3	⊢ ( 𝑥 = 𝐴 → ( 𝑓 : 𝑦 ⟶ 𝑥 ↔ 𝑓 : 𝑦 ⟶ 𝐴 ) )
6	5	abbidv	⊢ ( 𝑥 = 𝐴 → { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝑥 } = { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝐴 } )
7		feq2	⊢ ( 𝑦 = 𝐵 → ( 𝑓 : 𝑦 ⟶ 𝐴 ↔ 𝑓 : 𝐵 ⟶ 𝐴 ) )
8	7	abbidv	⊢ ( 𝑦 = 𝐵 → { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝐴 } = { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } )
9		df-map	⊢ ↑m = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ { 𝑓 ∣ 𝑓 : 𝑦 ⟶ 𝑥 } )
10	6 8 9	ovmpog	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } ∈ V ) → ( 𝐴 ↑m 𝐵 ) = { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } )
11	10	3expia	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } ∈ V → ( 𝐴 ↑m 𝐵 ) = { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } ) )
12	3 4 11	syl2an	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } ∈ V → ( 𝐴 ↑m 𝐵 ) = { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } ) )
13	2 12	mpd	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ↑m 𝐵 ) = { 𝑓 ∣ 𝑓 : 𝐵 ⟶ 𝐴 } )