Metamath Proof Explorer

Theorem mptprop

Description: Rewrite pairs of ordered pairs as mapping to functions. (Contributed by Thierry Arnoux, 24-Sep-2023)

Ref Expression
Hypotheses brprop.a 
|- ( ph -> A e. V )
brprop.b 
|- ( ph -> B e. W )
brprop.c 
|- ( ph -> C e. V )
brprop.d 
|- ( ph -> D e. W )
mptprop.1 
|- ( ph -> A =/= C )
Assertion mptprop 
|- ( ph -> { <. A , B >. , <. C , D >. } = ( x e. { A , C } |-> if ( x = A , B , D ) ) )

Proof

Step Hyp Ref Expression
1 brprop.a 
 |-  ( ph -> A e. V )
2 brprop.b 
 |-  ( ph -> B e. W )
3 brprop.c 
 |-  ( ph -> C e. V )
4 brprop.d 
 |-  ( ph -> D e. W )
5 mptprop.1 
 |-  ( ph -> A =/= C )
6 df-pr 
 |-  { <. A , B >. , <. C , D >. } = ( { <. A , B >. } u. { <. C , D >. } )
7 fmptsn 
 |-  ( ( A e. V /\ B e. W ) -> { <. A , B >. } = ( x e. { A } |-> B ) )
8 1 2 7 syl2anc 
 |-  ( ph -> { <. A , B >. } = ( x e. { A } |-> B ) )
9 incom 
 |-  ( { A } i^i { A , C } ) = ( { A , C } i^i { A } )
10 prid1g 
 |-  ( A e. V -> A e. { A , C } )
11 snssi 
 |-  ( A e. { A , C } -> { A } C_ { A , C } )
12 1 10 11 3syl 
 |-  ( ph -> { A } C_ { A , C } )
13 df-ss 
 |-  ( { A } C_ { A , C } <-> ( { A } i^i { A , C } ) = { A } )
14 12 13 sylib 
 |-  ( ph -> ( { A } i^i { A , C } ) = { A } )
15 9 14 eqtr3id 
 |-  ( ph -> ( { A , C } i^i { A } ) = { A } )
16 15 mpteq1d 
 |-  ( ph -> ( x e. ( { A , C } i^i { A } ) |-> B ) = ( x e. { A } |-> B ) )
17 8 16 eqtr4d 
 |-  ( ph -> { <. A , B >. } = ( x e. ( { A , C } i^i { A } ) |-> B ) )
18 fmptsn 
 |-  ( ( C e. V /\ D e. W ) -> { <. C , D >. } = ( x e. { C } |-> D ) )
19 3 4 18 syl2anc 
 |-  ( ph -> { <. C , D >. } = ( x e. { C } |-> D ) )
20 difprsn1 
 |-  ( A =/= C -> ( { A , C } \ { A } ) = { C } )
21 5 20 syl 
 |-  ( ph -> ( { A , C } \ { A } ) = { C } )
22 21 mpteq1d 
 |-  ( ph -> ( x e. ( { A , C } \ { A } ) |-> D ) = ( x e. { C } |-> D ) )
23 19 22 eqtr4d 
 |-  ( ph -> { <. C , D >. } = ( x e. ( { A , C } \ { A } ) |-> D ) )
24 17 23 uneq12d 
 |-  ( ph -> ( { <. A , B >. } u. { <. C , D >. } ) = ( ( x e. ( { A , C } i^i { A } ) |-> B ) u. ( x e. ( { A , C } \ { A } ) |-> D ) ) )
25 partfun 
 |-  ( x e. { A , C } |-> if ( x e. { A } , B , D ) ) = ( ( x e. ( { A , C } i^i { A } ) |-> B ) u. ( x e. ( { A , C } \ { A } ) |-> D ) )
26 24 25 eqtr4di 
 |-  ( ph -> ( { <. A , B >. } u. { <. C , D >. } ) = ( x e. { A , C } |-> if ( x e. { A } , B , D ) ) )
27 elsn2g 
 |-  ( A e. V -> ( x e. { A } <-> x = A ) )
28 1 27 syl 
 |-  ( ph -> ( x e. { A } <-> x = A ) )
29 28 ifbid 
 |-  ( ph -> if ( x e. { A } , B , D ) = if ( x = A , B , D ) )
30 29 mpteq2dv 
 |-  ( ph -> ( x e. { A , C } |-> if ( x e. { A } , B , D ) ) = ( x e. { A , C } |-> if ( x = A , B , D ) ) )
31 26 30 eqtrd 
 |-  ( ph -> ( { <. A , B >. } u. { <. C , D >. } ) = ( x e. { A , C } |-> if ( x = A , B , D ) ) )
32 6 31 syl5eq 
 |-  ( ph -> { <. A , B >. , <. C , D >. } = ( x e. { A , C } |-> if ( x = A , B , D ) ) )