Metamath Proof Explorer

Theorem opabiota

Description: Define a function whose value is "the unique y such that ph ( x , y ) ". (Contributed by NM, 16-Nov-2013)

Ref Expression
Hypotheses opabiota.1 
|- F = { <. x , y >. | { y | ph } = { y } }
opabiota.2 
|- ( x = B -> ( ph <-> ps ) )
Assertion opabiota 
|- ( B e. dom F -> ( F ` B ) = ( iota y ps ) )

Proof

Step Hyp Ref Expression
1 opabiota.1 
 |-  F = { <. x , y >. | { y | ph } = { y } }
2 opabiota.2 
 |-  ( x = B -> ( ph <-> ps ) )
3 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
4 2 iotabidv 
 |-  ( x = B -> ( iota y ph ) = ( iota y ps ) )
5 3 4 eqeq12d 
 |-  ( x = B -> ( ( F ` x ) = ( iota y ph ) <-> ( F ` B ) = ( iota y ps ) ) )
6 vex 
 |-  x e. _V
7 6 eldm 
 |-  ( x e. dom F <-> E. y x F y )
8 nfiota1 
 |-  F/_ y ( iota y ph )
9 8 nfeq2 
 |-  F/ y ( F ` x ) = ( iota y ph )
10 1 opabiotafun 
 |-  Fun F
11 funbrfv 
 |-  ( Fun F -> ( x F y -> ( F ` x ) = y ) )
12 10 11 ax-mp 
 |-  ( x F y -> ( F ` x ) = y )
13 df-br 
 |-  ( x F y <-> <. x , y >. e. F )
14 1 eleq2i 
 |-  ( <. x , y >. e. F <-> <. x , y >. e. { <. x , y >. | { y | ph } = { y } } )
15 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | { y | ph } = { y } } <-> { y | ph } = { y } )
16 13 14 15 3bitri 
 |-  ( x F y <-> { y | ph } = { y } )
17 vsnid 
 |-  y e. { y }
18 id 
 |-  ( { y | ph } = { y } -> { y | ph } = { y } )
19 17 18 eleqtrrid 
 |-  ( { y | ph } = { y } -> y e. { y | ph } )
20 abid 
 |-  ( y e. { y | ph } <-> ph )
21 19 20 sylib 
 |-  ( { y | ph } = { y } -> ph )
22 16 21 sylbi 
 |-  ( x F y -> ph )
23 vex 
 |-  y e. _V
24 6 23 breldm 
 |-  ( x F y -> x e. dom F )
25 1 opabiotadm 
 |-  dom F = { x | E! y ph }
26 25 eqabri 
 |-  ( x e. dom F <-> E! y ph )
27 24 26 sylib 
 |-  ( x F y -> E! y ph )
28 iota1 
 |-  ( E! y ph -> ( ph <-> ( iota y ph ) = y ) )
29 27 28 syl 
 |-  ( x F y -> ( ph <-> ( iota y ph ) = y ) )
30 22 29 mpbid 
 |-  ( x F y -> ( iota y ph ) = y )
31 12 30 eqtr4d 
 |-  ( x F y -> ( F ` x ) = ( iota y ph ) )
32 9 31 exlimi 
 |-  ( E. y x F y -> ( F ` x ) = ( iota y ph ) )
33 7 32 sylbi 
 |-  ( x e. dom F -> ( F ` x ) = ( iota y ph ) )
34 5 33 vtoclga 
 |-  ( B e. dom F -> ( F ` B ) = ( iota y ps ) )