This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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