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 | |
|
ssmapsn.a | |
||
ssmapsn.c | |
||
ssmapsn.d | |
||
Assertion | ssmapsn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssmapsn.f | |
|
2 | ssmapsn.a | |
|
3 | ssmapsn.c | |
|
4 | ssmapsn.d | |
|
5 | 3 | sselda | |
6 | elmapi | |
|
7 | 5 6 | syl | |
8 | 7 | ffnd | |
9 | 4 | a1i | |
10 | ovexd | |
|
11 | 10 3 | ssexd | |
12 | rnexg | |
|
13 | 12 | rgen | |
14 | 13 | a1i | |
15 | 11 14 | jca | |
16 | iunexg | |
|
17 | 15 16 | syl | |
18 | 9 17 | eqeltrd | |
19 | 18 | adantr | |
20 | ssiun2 | |
|
21 | 20 | adantl | |
22 | snidg | |
|
23 | 2 22 | syl | |
24 | 23 | adantr | |
25 | fnfvelrn | |
|
26 | 8 24 25 | syl2anc | |
27 | 21 26 | sseldd | |
28 | 27 4 | eleqtrrdi | |
29 | 8 19 28 | elmapsnd | |
30 | 29 | ex | |
31 | 18 | adantr | |
32 | snex | |
|
33 | 32 | a1i | |
34 | simpr | |
|
35 | 23 | adantr | |
36 | 31 33 34 35 | fvmap | |
37 | 4 | idi | |
38 | rneq | |
|
39 | 38 | cbviunv | |
40 | 37 39 | eqtri | |
41 | 36 40 | eleqtrdi | |
42 | eliun | |
|
43 | 41 42 | sylib | |
44 | simp3 | |
|
45 | simp1l | |
|
46 | 45 2 | syl | |
47 | eqid | |
|
48 | simp1r | |
|
49 | elmapfn | |
|
50 | 48 49 | syl | |
51 | 3 | sselda | |
52 | elmapfn | |
|
53 | 51 52 | syl | |
54 | 53 | 3adant3 | |
55 | 54 | 3adant1r | |
56 | 46 47 50 55 | fsneqrn | |
57 | 44 56 | mpbird | |
58 | simp2 | |
|
59 | 57 58 | eqeltrd | |
60 | 59 | 3exp | |
61 | 60 | rexlimdv | |
62 | 43 61 | mpd | |
63 | 62 | ex | |
64 | 30 63 | impbid | |
65 | 64 | alrimiv | |
66 | nfcv | |
|
67 | nfcv | |
|
68 | nfcv | |
|
69 | 1 67 68 | nfov | |
70 | 66 69 | cleqf | |
71 | 65 70 | sylibr | |