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

Metamath Proof Explorer

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 𝐵 } )