Theorem mapval2

Description: Alternate expression for the value of set exponentiation. (Contributed by NM, 3-Nov-2007)

	Ref	Expression
Hypotheses	elmap.1	⊢ 𝐴 ∈ V
	elmap.2	⊢ 𝐵 ∈ V
Assertion	mapval2	⊢ ( 𝐴 ↑m 𝐵 ) = ( 𝒫 ( 𝐵 × 𝐴 ) ∩ { 𝑓 ∣ 𝑓 Fn 𝐵 } )

Proof

Step	Hyp	Ref	Expression
1		elmap.1	⊢ 𝐴 ∈ V
2		elmap.2	⊢ 𝐵 ∈ V
3		dff2	⊢ ( 𝑔 : 𝐵 ⟶ 𝐴 ↔ ( 𝑔 Fn 𝐵 ∧ 𝑔 ⊆ ( 𝐵 × 𝐴 ) ) )
4	3	biancomi	⊢ ( 𝑔 : 𝐵 ⟶ 𝐴 ↔ ( 𝑔 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑔 Fn 𝐵 ) )
5	1 2	elmap	⊢ ( 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝑔 : 𝐵 ⟶ 𝐴 )
6		elin	⊢ ( 𝑔 ∈ ( 𝒫 ( 𝐵 × 𝐴 ) ∩ { 𝑓 ∣ 𝑓 Fn 𝐵 } ) ↔ ( 𝑔 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∧ 𝑔 ∈ { 𝑓 ∣ 𝑓 Fn 𝐵 } ) )
7		velpw	⊢ ( 𝑔 ∈ 𝒫 ( 𝐵 × 𝐴 ) ↔ 𝑔 ⊆ ( 𝐵 × 𝐴 ) )
8		vex	⊢ 𝑔 ∈ V
9		fneq1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 Fn 𝐵 ↔ 𝑔 Fn 𝐵 ) )
10	8 9	elab	⊢ ( 𝑔 ∈ { 𝑓 ∣ 𝑓 Fn 𝐵 } ↔ 𝑔 Fn 𝐵 )
11	7 10	anbi12i	⊢ ( ( 𝑔 ∈ 𝒫 ( 𝐵 × 𝐴 ) ∧ 𝑔 ∈ { 𝑓 ∣ 𝑓 Fn 𝐵 } ) ↔ ( 𝑔 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑔 Fn 𝐵 ) )
12	6 11	bitri	⊢ ( 𝑔 ∈ ( 𝒫 ( 𝐵 × 𝐴 ) ∩ { 𝑓 ∣ 𝑓 Fn 𝐵 } ) ↔ ( 𝑔 ⊆ ( 𝐵 × 𝐴 ) ∧ 𝑔 Fn 𝐵 ) )
13	4 5 12	3bitr4i	⊢ ( 𝑔 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝑔 ∈ ( 𝒫 ( 𝐵 × 𝐴 ) ∩ { 𝑓 ∣ 𝑓 Fn 𝐵 } ) )
14	13	eqriv	⊢ ( 𝐴 ↑m 𝐵 ) = ( 𝒫 ( 𝐵 × 𝐴 ) ∩ { 𝑓 ∣ 𝑓 Fn 𝐵 } )