Metamath Proof Explorer

Theorem mposn

Description: An operation (in maps-to notation) on two singletons. (Contributed by AV, 4-Aug-2019)

Ref Expression
Hypotheses mposn.f 
|- F = ( x e. { A } , y e. { B } |-> C )
mposn.a 
|- ( x = A -> C = D )
mposn.b 
|- ( y = B -> D = E )
Assertion mposn 
|- ( ( A e. V /\ B e. W /\ E e. U ) -> F = { <. <. A , B >. , E >. } )

Proof

Step Hyp Ref Expression
1 mposn.f 
 |-  F = ( x e. { A } , y e. { B } |-> C )
2 mposn.a 
 |-  ( x = A -> C = D )
3 mposn.b 
 |-  ( y = B -> D = E )
4 xpsng 
 |-  ( ( A e. V /\ B e. W ) -> ( { A } X. { B } ) = { <. A , B >. } )
5 4 3adant3 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> ( { A } X. { B } ) = { <. A , B >. } )
6 5 mpteq1d 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> ( p e. ( { A } X. { B } ) |-> [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C ) = ( p e. { <. A , B >. } |-> [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C ) )
7 mpompts 
 |-  ( x e. { A } , y e. { B } |-> C ) = ( p e. ( { A } X. { B } ) |-> [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C )
8 1 7 eqtri 
 |-  F = ( p e. ( { A } X. { B } ) |-> [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C )
9 8 a1i 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> F = ( p e. ( { A } X. { B } ) |-> [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C ) )
10 op2ndg 
 |-  ( ( A e. V /\ B e. W ) -> ( 2nd ` <. A , B >. ) = B )
11 fveq2 
 |-  ( p = <. A , B >. -> ( 2nd ` p ) = ( 2nd ` <. A , B >. ) )
12 11 eqcomd 
 |-  ( p = <. A , B >. -> ( 2nd ` <. A , B >. ) = ( 2nd ` p ) )
13 12 eqeq1d 
 |-  ( p = <. A , B >. -> ( ( 2nd ` <. A , B >. ) = B <-> ( 2nd ` p ) = B ) )
14 10 13 syl5ibcom 
 |-  ( ( A e. V /\ B e. W ) -> ( p = <. A , B >. -> ( 2nd ` p ) = B ) )
15 14 3adant3 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> ( p = <. A , B >. -> ( 2nd ` p ) = B ) )
16 15 imp 
 |-  ( ( ( A e. V /\ B e. W /\ E e. U ) /\ p = <. A , B >. ) -> ( 2nd ` p ) = B )
17 op1stg 
 |-  ( ( A e. V /\ B e. W ) -> ( 1st ` <. A , B >. ) = A )
18 fveq2 
 |-  ( p = <. A , B >. -> ( 1st ` p ) = ( 1st ` <. A , B >. ) )
19 18 eqcomd 
 |-  ( p = <. A , B >. -> ( 1st ` <. A , B >. ) = ( 1st ` p ) )
20 19 eqeq1d 
 |-  ( p = <. A , B >. -> ( ( 1st ` <. A , B >. ) = A <-> ( 1st ` p ) = A ) )
21 17 20 syl5ibcom 
 |-  ( ( A e. V /\ B e. W ) -> ( p = <. A , B >. -> ( 1st ` p ) = A ) )
22 21 3adant3 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> ( p = <. A , B >. -> ( 1st ` p ) = A ) )
23 22 imp 
 |-  ( ( ( A e. V /\ B e. W /\ E e. U ) /\ p = <. A , B >. ) -> ( 1st ` p ) = A )
24 simp1 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> A e. V )
25 simpl2 
 |-  ( ( ( A e. V /\ B e. W /\ E e. U ) /\ x = A ) -> B e. W )
26 2 adantl 
 |-  ( ( ( A e. V /\ B e. W /\ E e. U ) /\ x = A ) -> C = D )
27 26 3 sylan9eq 
 |-  ( ( ( ( A e. V /\ B e. W /\ E e. U ) /\ x = A ) /\ y = B ) -> C = E )
28 25 27 csbied 
 |-  ( ( ( A e. V /\ B e. W /\ E e. U ) /\ x = A ) -> [_ B / y ]_ C = E )
29 24 28 csbied 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> [_ A / x ]_ [_ B / y ]_ C = E )
30 29 adantr 
 |-  ( ( ( A e. V /\ B e. W /\ E e. U ) /\ p = <. A , B >. ) -> [_ A / x ]_ [_ B / y ]_ C = E )
31 csbeq1 
 |-  ( ( 1st ` p ) = A -> [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C = [_ A / x ]_ [_ ( 2nd ` p ) / y ]_ C )
32 31 eqeq1d 
 |-  ( ( 1st ` p ) = A -> ( [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C = E <-> [_ A / x ]_ [_ ( 2nd ` p ) / y ]_ C = E ) )
33 32 adantl 
 |-  ( ( ( 2nd ` p ) = B /\ ( 1st ` p ) = A ) -> ( [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C = E <-> [_ A / x ]_ [_ ( 2nd ` p ) / y ]_ C = E ) )
34 csbeq1 
 |-  ( ( 2nd ` p ) = B -> [_ ( 2nd ` p ) / y ]_ C = [_ B / y ]_ C )
35 34 adantr 
 |-  ( ( ( 2nd ` p ) = B /\ ( 1st ` p ) = A ) -> [_ ( 2nd ` p ) / y ]_ C = [_ B / y ]_ C )
36 35 csbeq2dv 
 |-  ( ( ( 2nd ` p ) = B /\ ( 1st ` p ) = A ) -> [_ A / x ]_ [_ ( 2nd ` p ) / y ]_ C = [_ A / x ]_ [_ B / y ]_ C )
37 36 eqeq1d 
 |-  ( ( ( 2nd ` p ) = B /\ ( 1st ` p ) = A ) -> ( [_ A / x ]_ [_ ( 2nd ` p ) / y ]_ C = E <-> [_ A / x ]_ [_ B / y ]_ C = E ) )
38 33 37 bitrd 
 |-  ( ( ( 2nd ` p ) = B /\ ( 1st ` p ) = A ) -> ( [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C = E <-> [_ A / x ]_ [_ B / y ]_ C = E ) )
39 30 38 syl5ibrcom 
 |-  ( ( ( A e. V /\ B e. W /\ E e. U ) /\ p = <. A , B >. ) -> ( ( ( 2nd ` p ) = B /\ ( 1st ` p ) = A ) -> [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C = E ) )
40 16 23 39 mp2and 
 |-  ( ( ( A e. V /\ B e. W /\ E e. U ) /\ p = <. A , B >. ) -> [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C = E )
41 opex 
 |-  <. A , B >. e. _V
42 41 a1i 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> <. A , B >. e. _V )
43 simp3 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> E e. U )
44 40 42 43 fmptsnd 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> { <. <. A , B >. , E >. } = ( p e. { <. A , B >. } |-> [_ ( 1st ` p ) / x ]_ [_ ( 2nd ` p ) / y ]_ C ) )
45 6 9 44 3eqtr4d 
 |-  ( ( A e. V /\ B e. W /\ E e. U ) -> F = { <. <. A , B >. , E >. } )