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 
|- A e. _V
elmap.2 
|- B e. _V
Assertion mapval2 
|- ( A ^m B ) = ( ~P ( B X. A ) i^i { f | f Fn B } )

Proof

Step Hyp Ref Expression
1 elmap.1 
 |-  A e. _V
2 elmap.2 
 |-  B e. _V
3 dff2 
 |-  ( g : B --> A <-> ( g Fn B /\ g C_ ( B X. A ) ) )
4 3 biancomi 
 |-  ( g : B --> A <-> ( g C_ ( B X. A ) /\ g Fn B ) )
5 1 2 elmap 
 |-  ( g e. ( A ^m B ) <-> g : B --> A )
6 elin 
 |-  ( g e. ( ~P ( B X. A ) i^i { f | f Fn B } ) <-> ( g e. ~P ( B X. A ) /\ g e. { f | f Fn B } ) )
7 velpw 
 |-  ( g e. ~P ( B X. A ) <-> g C_ ( B X. A ) )
8 vex 
 |-  g e. _V
9 fneq1 
 |-  ( f = g -> ( f Fn B <-> g Fn B ) )
10 8 9 elab 
 |-  ( g e. { f | f Fn B } <-> g Fn B )
11 7 10 anbi12i 
 |-  ( ( g e. ~P ( B X. A ) /\ g e. { f | f Fn B } ) <-> ( g C_ ( B X. A ) /\ g Fn B ) )
12 6 11 bitri 
 |-  ( g e. ( ~P ( B X. A ) i^i { f | f Fn B } ) <-> ( g C_ ( B X. A ) /\ g Fn B ) )
13 4 5 12 3bitr4i 
 |-  ( g e. ( A ^m B ) <-> g e. ( ~P ( B X. A ) i^i { f | f Fn B } ) )
14 13 eqriv 
 |-  ( A ^m B ) = ( ~P ( B X. A ) i^i { f | f Fn B } )