Metamath Proof Explorer


Theorem ssmapsn

Description: A subset C of a set exponentiation to a singleton, is its projection D exponentiated to the singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses ssmapsn.f _fD
ssmapsn.a φAV
ssmapsn.c φCBA
ssmapsn.d D=fCranf
Assertion ssmapsn φC=DA

Proof

Step Hyp Ref Expression
1 ssmapsn.f _fD
2 ssmapsn.a φAV
3 ssmapsn.c φCBA
4 ssmapsn.d D=fCranf
5 3 sselda φfCfBA
6 elmapi fBAf:AB
7 5 6 syl φfCf:AB
8 7 ffnd φfCfFnA
9 4 a1i φD=fCranf
10 ovexd φBAV
11 10 3 ssexd φCV
12 rnexg fCranfV
13 12 rgen fCranfV
14 13 a1i φfCranfV
15 11 14 jca φCVfCranfV
16 iunexg CVfCranfVfCranfV
17 15 16 syl φfCranfV
18 9 17 eqeltrd φDV
19 18 adantr φfCDV
20 ssiun2 fCranffCranf
21 20 adantl φfCranffCranf
22 snidg AVAA
23 2 22 syl φAA
24 23 adantr φfCAA
25 fnfvelrn fFnAAAfAranf
26 8 24 25 syl2anc φfCfAranf
27 21 26 sseldd φfCfAfCranf
28 27 4 eleqtrrdi φfCfAD
29 8 19 28 elmapsnd φfCfDA
30 29 ex φfCfDA
31 18 adantr φfDADV
32 snex AV
33 32 a1i φfDAAV
34 simpr φfDAfDA
35 23 adantr φfDAAA
36 31 33 34 35 fvmap φfDAfAD
37 4 idi D=fCranf
38 rneq f=granf=rang
39 38 cbviunv fCranf=gCrang
40 37 39 eqtri D=gCrang
41 36 40 eleqtrdi φfDAfAgCrang
42 eliun fAgCranggCfArang
43 41 42 sylib φfDAgCfArang
44 simp3 φfDAgCfArangfArang
45 simp1l φfDAgCfArangφ
46 45 2 syl φfDAgCfArangAV
47 eqid A=A
48 simp1r φfDAgCfArangfDA
49 elmapfn fDAfFnA
50 48 49 syl φfDAgCfArangfFnA
51 3 sselda φgCgBA
52 elmapfn gBAgFnA
53 51 52 syl φgCgFnA
54 53 3adant3 φgCfAranggFnA
55 54 3adant1r φfDAgCfAranggFnA
56 46 47 50 55 fsneqrn φfDAgCfArangf=gfArang
57 44 56 mpbird φfDAgCfArangf=g
58 simp2 φfDAgCfAranggC
59 57 58 eqeltrd φfDAgCfArangfC
60 59 3exp φfDAgCfArangfC
61 60 rexlimdv φfDAgCfArangfC
62 43 61 mpd φfDAfC
63 62 ex φfDAfC
64 30 63 impbid φfCfDA
65 64 alrimiv φffCfDA
66 nfcv _fC
67 nfcv _f𝑚
68 nfcv _fA
69 1 67 68 nfov _fDA
70 66 69 cleqf C=DAffCfDA
71 65 70 sylibr φC=DA