Metamath Proof Explorer

Theorem mapsncnv

Description: Expression for the inverse of the canonical map between a set and its set of singleton functions. (Contributed by Stefan O'Rear, 21-Mar-2015)

Ref Expression
Hypotheses mapsncnv.s 
|- S = { X }
mapsncnv.b 
|- B e. _V
mapsncnv.x 
|- X e. _V
mapsncnv.f 
|- F = ( x e. ( B ^m S ) |-> ( x ` X ) )
Assertion mapsncnv 
|- `' F = ( y e. B |-> ( S X. { y } ) )

Proof

Step Hyp Ref Expression
1 mapsncnv.s 
 |-  S = { X }
2 mapsncnv.b 
 |-  B e. _V
3 mapsncnv.x 
 |-  X e. _V
4 mapsncnv.f 
 |-  F = ( x e. ( B ^m S ) |-> ( x ` X ) )
5 elmapi 
 |-  ( x e. ( B ^m { X } ) -> x : { X } --> B )
6 3 snid 
 |-  X e. { X }
7 ffvelrn 
 |-  ( ( x : { X } --> B /\ X e. { X } ) -> ( x ` X ) e. B )
8 5 6 7 sylancl 
 |-  ( x e. ( B ^m { X } ) -> ( x ` X ) e. B )
9 eqid 
 |-  { X } = { X }
10 9 2 3 mapsnconst 
 |-  ( x e. ( B ^m { X } ) -> x = ( { X } X. { ( x ` X ) } ) )
11 8 10 jca 
 |-  ( x e. ( B ^m { X } ) -> ( ( x ` X ) e. B /\ x = ( { X } X. { ( x ` X ) } ) ) )
12 eleq1 
 |-  ( y = ( x ` X ) -> ( y e. B <-> ( x ` X ) e. B ) )
13 sneq 
 |-  ( y = ( x ` X ) -> { y } = { ( x ` X ) } )
14 13 xpeq2d 
 |-  ( y = ( x ` X ) -> ( { X } X. { y } ) = ( { X } X. { ( x ` X ) } ) )
15 14 eqeq2d 
 |-  ( y = ( x ` X ) -> ( x = ( { X } X. { y } ) <-> x = ( { X } X. { ( x ` X ) } ) ) )
16 12 15 anbi12d 
 |-  ( y = ( x ` X ) -> ( ( y e. B /\ x = ( { X } X. { y } ) ) <-> ( ( x ` X ) e. B /\ x = ( { X } X. { ( x ` X ) } ) ) ) )
17 11 16 syl5ibrcom 
 |-  ( x e. ( B ^m { X } ) -> ( y = ( x ` X ) -> ( y e. B /\ x = ( { X } X. { y } ) ) ) )
18 17 imp 
 |-  ( ( x e. ( B ^m { X } ) /\ y = ( x ` X ) ) -> ( y e. B /\ x = ( { X } X. { y } ) ) )
19 fconst6g 
 |-  ( y e. B -> ( { X } X. { y } ) : { X } --> B )
20 snex 
 |-  { X } e. _V
21 2 20 elmap 
 |-  ( ( { X } X. { y } ) e. ( B ^m { X } ) <-> ( { X } X. { y } ) : { X } --> B )
22 19 21 sylibr 
 |-  ( y e. B -> ( { X } X. { y } ) e. ( B ^m { X } ) )
23 vex 
 |-  y e. _V
24 23 fvconst2 
 |-  ( X e. { X } -> ( ( { X } X. { y } ) ` X ) = y )
25 6 24 mp1i 
 |-  ( y e. B -> ( ( { X } X. { y } ) ` X ) = y )
26 25 eqcomd 
 |-  ( y e. B -> y = ( ( { X } X. { y } ) ` X ) )
27 22 26 jca 
 |-  ( y e. B -> ( ( { X } X. { y } ) e. ( B ^m { X } ) /\ y = ( ( { X } X. { y } ) ` X ) ) )
28 eleq1 
 |-  ( x = ( { X } X. { y } ) -> ( x e. ( B ^m { X } ) <-> ( { X } X. { y } ) e. ( B ^m { X } ) ) )
29 fveq1 
 |-  ( x = ( { X } X. { y } ) -> ( x ` X ) = ( ( { X } X. { y } ) ` X ) )
30 29 eqeq2d 
 |-  ( x = ( { X } X. { y } ) -> ( y = ( x ` X ) <-> y = ( ( { X } X. { y } ) ` X ) ) )
31 28 30 anbi12d 
 |-  ( x = ( { X } X. { y } ) -> ( ( x e. ( B ^m { X } ) /\ y = ( x ` X ) ) <-> ( ( { X } X. { y } ) e. ( B ^m { X } ) /\ y = ( ( { X } X. { y } ) ` X ) ) ) )
32 27 31 syl5ibrcom 
 |-  ( y e. B -> ( x = ( { X } X. { y } ) -> ( x e. ( B ^m { X } ) /\ y = ( x ` X ) ) ) )
33 32 imp 
 |-  ( ( y e. B /\ x = ( { X } X. { y } ) ) -> ( x e. ( B ^m { X } ) /\ y = ( x ` X ) ) )
34 18 33 impbii 
 |-  ( ( x e. ( B ^m { X } ) /\ y = ( x ` X ) ) <-> ( y e. B /\ x = ( { X } X. { y } ) ) )
35 1 oveq2i 
 |-  ( B ^m S ) = ( B ^m { X } )
36 35 eleq2i 
 |-  ( x e. ( B ^m S ) <-> x e. ( B ^m { X } ) )
37 36 anbi1i 
 |-  ( ( x e. ( B ^m S ) /\ y = ( x ` X ) ) <-> ( x e. ( B ^m { X } ) /\ y = ( x ` X ) ) )
38 1 xpeq1i 
 |-  ( S X. { y } ) = ( { X } X. { y } )
39 38 eqeq2i 
 |-  ( x = ( S X. { y } ) <-> x = ( { X } X. { y } ) )
40 39 anbi2i 
 |-  ( ( y e. B /\ x = ( S X. { y } ) ) <-> ( y e. B /\ x = ( { X } X. { y } ) ) )
41 34 37 40 3bitr4i 
 |-  ( ( x e. ( B ^m S ) /\ y = ( x ` X ) ) <-> ( y e. B /\ x = ( S X. { y } ) ) )
42 41 opabbii 
 |-  { <. y , x >. | ( x e. ( B ^m S ) /\ y = ( x ` X ) ) } = { <. y , x >. | ( y e. B /\ x = ( S X. { y } ) ) }
43 df-mpt 
 |-  ( x e. ( B ^m S ) |-> ( x ` X ) ) = { <. x , y >. | ( x e. ( B ^m S ) /\ y = ( x ` X ) ) }
44 4 43 eqtri 
 |-  F = { <. x , y >. | ( x e. ( B ^m S ) /\ y = ( x ` X ) ) }
45 44 cnveqi 
 |-  `' F = `' { <. x , y >. | ( x e. ( B ^m S ) /\ y = ( x ` X ) ) }
46 cnvopab 
 |-  `' { <. x , y >. | ( x e. ( B ^m S ) /\ y = ( x ` X ) ) } = { <. y , x >. | ( x e. ( B ^m S ) /\ y = ( x ` X ) ) }
47 45 46 eqtri 
 |-  `' F = { <. y , x >. | ( x e. ( B ^m S ) /\ y = ( x ` X ) ) }
48 df-mpt 
 |-  ( y e. B |-> ( S X. { y } ) ) = { <. y , x >. | ( y e. B /\ x = ( S X. { y } ) ) }
49 42 47 48 3eqtr4i 
 |-  `' F = ( y e. B |-> ( S X. { y } ) )