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}=\left\{{X}\right\}$
mapsncnv.b ${⊢}{B}\in \mathrm{V}$
mapsncnv.x ${⊢}{X}\in \mathrm{V}$
mapsncnv.f ${⊢}{F}=\left({x}\in \left({{B}}^{{S}}\right)⟼{x}\left({X}\right)\right)$
Assertion mapsncnv ${⊢}{{F}}^{-1}=\left({y}\in {B}⟼{S}×\left\{{y}\right\}\right)$

Proof

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