Metamath Proof Explorer

Theorem fmptsnd

Description: Express a singleton function in maps-to notation. Deduction form of fmptsng . (Contributed by AV, 4-Aug-2019)

Ref Expression
Hypotheses fmptsnd.1 
|- ( ( ph /\ x = A ) -> B = C )
fmptsnd.2 
|- ( ph -> A e. V )
fmptsnd.3 
|- ( ph -> C e. W )
Assertion fmptsnd 
|- ( ph -> { <. A , C >. } = ( x e. { A } |-> B ) )

Proof

Step Hyp Ref Expression
1 fmptsnd.1 
 |-  ( ( ph /\ x = A ) -> B = C )
2 fmptsnd.2 
 |-  ( ph -> A e. V )
3 fmptsnd.3 
 |-  ( ph -> C e. W )
4 velsn 
 |-  ( x e. { A } <-> x = A )
5 4 bicomi 
 |-  ( x = A <-> x e. { A } )
6 5 anbi1i 
 |-  ( ( x = A /\ y = B ) <-> ( x e. { A } /\ y = B ) )
7 6 opabbii 
 |-  { <. x , y >. | ( x = A /\ y = B ) } = { <. x , y >. | ( x e. { A } /\ y = B ) }
8 velsn 
 |-  ( p e. { <. A , C >. } <-> p = <. A , C >. )
9 eqidd 
 |-  ( ph -> A = A )
10 eqidd 
 |-  ( ph -> C = C )
11 sbcan 
 |-  ( [. C / y ]. ( x = A /\ y = B ) <-> ( [. C / y ]. x = A /\ [. C / y ]. y = B ) )
12 sbcg 
 |-  ( C e. W -> ( [. C / y ]. x = A <-> x = A ) )
13 3 12 syl 
 |-  ( ph -> ( [. C / y ]. x = A <-> x = A ) )
14 eqsbc1 
 |-  ( C e. W -> ( [. C / y ]. y = B <-> C = B ) )
15 3 14 syl 
 |-  ( ph -> ( [. C / y ]. y = B <-> C = B ) )
16 13 15 anbi12d 
 |-  ( ph -> ( ( [. C / y ]. x = A /\ [. C / y ]. y = B ) <-> ( x = A /\ C = B ) ) )
17 11 16 bitrid 
 |-  ( ph -> ( [. C / y ]. ( x = A /\ y = B ) <-> ( x = A /\ C = B ) ) )
18 17 sbcbidv 
 |-  ( ph -> ( [. A / x ]. [. C / y ]. ( x = A /\ y = B ) <-> [. A / x ]. ( x = A /\ C = B ) ) )
19 eqeq1 
 |-  ( x = A -> ( x = A <-> A = A ) )
20 19 adantl 
 |-  ( ( ph /\ x = A ) -> ( x = A <-> A = A ) )
21 1 eqeq2d 
 |-  ( ( ph /\ x = A ) -> ( C = B <-> C = C ) )
22 20 21 anbi12d 
 |-  ( ( ph /\ x = A ) -> ( ( x = A /\ C = B ) <-> ( A = A /\ C = C ) ) )
23 2 22 sbcied 
 |-  ( ph -> ( [. A / x ]. ( x = A /\ C = B ) <-> ( A = A /\ C = C ) ) )
24 18 23 bitrd 
 |-  ( ph -> ( [. A / x ]. [. C / y ]. ( x = A /\ y = B ) <-> ( A = A /\ C = C ) ) )
25 9 10 24 mpbir2and 
 |-  ( ph -> [. A / x ]. [. C / y ]. ( x = A /\ y = B ) )
26 opelopabsb 
 |-  ( <. A , C >. e. { <. x , y >. | ( x = A /\ y = B ) } <-> [. A / x ]. [. C / y ]. ( x = A /\ y = B ) )
27 25 26 sylibr 
 |-  ( ph -> <. A , C >. e. { <. x , y >. | ( x = A /\ y = B ) } )
28 eleq1 
 |-  ( p = <. A , C >. -> ( p e. { <. x , y >. | ( x = A /\ y = B ) } <-> <. A , C >. e. { <. x , y >. | ( x = A /\ y = B ) } ) )
29 27 28 syl5ibrcom 
 |-  ( ph -> ( p = <. A , C >. -> p e. { <. x , y >. | ( x = A /\ y = B ) } ) )
30 8 29 biimtrid 
 |-  ( ph -> ( p e. { <. A , C >. } -> p e. { <. x , y >. | ( x = A /\ y = B ) } ) )
31 elopab 
 |-  ( p e. { <. x , y >. | ( x = A /\ y = B ) } <-> E. x E. y ( p = <. x , y >. /\ ( x = A /\ y = B ) ) )
32 opeq12 
 |-  ( ( x = A /\ y = B ) -> <. x , y >. = <. A , B >. )
33 32 adantl 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> <. x , y >. = <. A , B >. )
34 33 eqeq2d 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( p = <. x , y >. <-> p = <. A , B >. ) )
35 1 adantrr 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> B = C )
36 35 opeq2d 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> <. A , B >. = <. A , C >. )
37 opex 
 |-  <. A , C >. e. _V
38 37 snid 
 |-  <. A , C >. e. { <. A , C >. }
39 36 38 eqeltrdi 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> <. A , B >. e. { <. A , C >. } )
40 eleq1 
 |-  ( p = <. A , B >. -> ( p e. { <. A , C >. } <-> <. A , B >. e. { <. A , C >. } ) )
41 39 40 syl5ibrcom 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( p = <. A , B >. -> p e. { <. A , C >. } ) )
42 34 41 sylbid 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( p = <. x , y >. -> p e. { <. A , C >. } ) )
43 42 ex 
 |-  ( ph -> ( ( x = A /\ y = B ) -> ( p = <. x , y >. -> p e. { <. A , C >. } ) ) )
44 43 impcomd 
 |-  ( ph -> ( ( p = <. x , y >. /\ ( x = A /\ y = B ) ) -> p e. { <. A , C >. } ) )
45 44 exlimdvv 
 |-  ( ph -> ( E. x E. y ( p = <. x , y >. /\ ( x = A /\ y = B ) ) -> p e. { <. A , C >. } ) )
46 31 45 biimtrid 
 |-  ( ph -> ( p e. { <. x , y >. | ( x = A /\ y = B ) } -> p e. { <. A , C >. } ) )
47 30 46 impbid 
 |-  ( ph -> ( p e. { <. A , C >. } <-> p e. { <. x , y >. | ( x = A /\ y = B ) } ) )
48 47 eqrdv 
 |-  ( ph -> { <. A , C >. } = { <. x , y >. | ( x = A /\ y = B ) } )
49 df-mpt 
 |-  ( x e. { A } |-> B ) = { <. x , y >. | ( x e. { A } /\ y = B ) }
50 49 a1i 
 |-  ( ph -> ( x e. { A } |-> B ) = { <. x , y >. | ( x e. { A } /\ y = B ) } )
51 7 48 50 3eqtr4a 
 |-  ( ph -> { <. A , C >. } = ( x e. { A } |-> B ) )