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

Metamath Proof Explorer

Theorem fmptpr

Description: Express a pair function in maps-to notation. (Contributed by Thierry Arnoux, 3-Jan-2017)

Ref Expression
Hypotheses fmptpr.1 
|- ( ph -> A e. V )
fmptpr.2 
|- ( ph -> B e. W )
fmptpr.3 
|- ( ph -> C e. X )
fmptpr.4 
|- ( ph -> D e. Y )
fmptpr.5 
|- ( ( ph /\ x = A ) -> E = C )
fmptpr.6 
|- ( ( ph /\ x = B ) -> E = D )
Assertion fmptpr 
|- ( ph -> { <. A , C >. , <. B , D >. } = ( x e. { A , B } |-> E ) )

Proof

Step Hyp Ref Expression
1 fmptpr.1 
 |-  ( ph -> A e. V )
2 fmptpr.2 
 |-  ( ph -> B e. W )
3 fmptpr.3 
 |-  ( ph -> C e. X )
4 fmptpr.4 
 |-  ( ph -> D e. Y )
5 fmptpr.5 
 |-  ( ( ph /\ x = A ) -> E = C )
6 fmptpr.6 
 |-  ( ( ph /\ x = B ) -> E = D )
7 df-pr 
 |-  { <. A , C >. , <. B , D >. } = ( { <. A , C >. } u. { <. B , D >. } )
8 7 a1i 
 |-  ( ph -> { <. A , C >. , <. B , D >. } = ( { <. A , C >. } u. { <. B , D >. } ) )
9 5 1 3 fmptsnd 
 |-  ( ph -> { <. A , C >. } = ( x e. { A } |-> E ) )
10 9 uneq1d 
 |-  ( ph -> ( { <. A , C >. } u. { <. B , D >. } ) = ( ( x e. { A } |-> E ) u. { <. B , D >. } ) )
11 df-pr 
 |-  { A , B } = ( { A } u. { B } )
12 11 eqcomi 
 |-  ( { A } u. { B } ) = { A , B }
13 12 a1i 
 |-  ( ph -> ( { A } u. { B } ) = { A , B } )
14 2 4 13 6 fmptapd 
 |-  ( ph -> ( ( x e. { A } |-> E ) u. { <. B , D >. } ) = ( x e. { A , B } |-> E ) )
15 8 10 14 3eqtrd 
 |-  ( ph -> { <. A , C >. , <. B , D >. } = ( x e. { A , B } |-> E ) )