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 _ f D
ssmapsn.a φ A V
ssmapsn.c φ C B A
ssmapsn.d D = f C ran f
Assertion ssmapsn φ C = D A

Proof

Step Hyp Ref Expression
1 ssmapsn.f _ f D
2 ssmapsn.a φ A V
3 ssmapsn.c φ C B A
4 ssmapsn.d D = f C ran f
5 3 sselda φ f C f B A
6 elmapi f B A f : A B
7 5 6 syl φ f C f : A B
8 7 ffnd φ f C f Fn A
9 4 a1i φ D = f C ran f
10 ovexd φ B A V
11 10 3 ssexd φ C V
12 rnexg f C ran f V
13 12 rgen f C ran f V
14 iunexg C V f C ran f V f C ran f V
15 11 13 14 sylancl φ f C ran f V
16 9 15 eqeltrd φ D V
17 16 adantr φ f C D V
18 ssiun2 f C ran f f C ran f
19 18 adantl φ f C ran f f C ran f
20 snidg A V A A
21 2 20 syl φ A A
22 21 adantr φ f C A A
23 8 22 fnfvelrnd φ f C f A ran f
24 19 23 sseldd φ f C f A f C ran f
25 24 4 eleqtrrdi φ f C f A D
26 8 17 25 elmapsnd φ f C f D A
27 16 adantr φ f D A D V
28 snex A V
29 28 a1i φ f D A A V
30 simpr φ f D A f D A
31 21 adantr φ f D A A A
32 27 29 30 31 fvmap φ f D A f A D
33 rneq f = g ran f = ran g
34 33 cbviunv f C ran f = g C ran g
35 4 34 eqtri D = g C ran g
36 32 35 eleqtrdi φ f D A f A g C ran g
37 eliun f A g C ran g g C f A ran g
38 36 37 sylib φ f D A g C f A ran g
39 simp3 φ f D A g C f A ran g f A ran g
40 simp1l φ f D A g C f A ran g φ
41 40 2 syl φ f D A g C f A ran g A V
42 eqid A = A
43 simp1r φ f D A g C f A ran g f D A
44 elmapfn f D A f Fn A
45 43 44 syl φ f D A g C f A ran g f Fn A
46 3 sselda φ g C g B A
47 elmapfn g B A g Fn A
48 46 47 syl φ g C g Fn A
49 48 3adant3 φ g C f A ran g g Fn A
50 49 3adant1r φ f D A g C f A ran g g Fn A
51 41 42 45 50 fsneqrn φ f D A g C f A ran g f = g f A ran g
52 39 51 mpbird φ f D A g C f A ran g f = g
53 simp2 φ f D A g C f A ran g g C
54 52 53 eqeltrd φ f D A g C f A ran g f C
55 54 rexlimdv3a φ f D A g C f A ran g f C
56 38 55 mpd φ f D A f C
57 26 56 impbida φ f C f D A
58 57 alrimiv φ f f C f D A
59 nfcv _ f C
60 nfcv _ f 𝑚
61 nfcv _ f A
62 1 60 61 nfov _ f D A
63 59 62 cleqf C = D A f f C f D A
64 58 63 sylibr φ C = D A