Metamath Proof Explorer


Theorem mapsnd

Description: The value of set exponentiation with a singleton exponent. Theorem 98 of Suppes p. 89. (Contributed by NM, 10-Dec-2003) (Revised by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses mapsnd.1 φ A V
mapsnd.2 φ B W
Assertion mapsnd φ A B = f | y A f = B y

Proof

Step Hyp Ref Expression
1 mapsnd.1 φ A V
2 mapsnd.2 φ B W
3 snex B V
4 3 a1i φ B V
5 1 4 elmapd φ f A B f : B A
6 ffn f : B A f Fn B
7 snidg B W B B
8 2 7 syl φ B B
9 fneu f Fn B B B ∃! y B f y
10 6 8 9 syl2anr φ f : B A ∃! y B f y
11 euabsn ∃! y B f y y y | B f y = y
12 frel f : B A Rel f
13 relimasn Rel f f B = y | B f y
14 12 13 syl f : B A f B = y | B f y
15 fdm f : B A dom f = B
16 15 imaeq2d f : B A f dom f = f B
17 imadmrn f dom f = ran f
18 16 17 eqtr3di f : B A f B = ran f
19 14 18 eqtr3d f : B A y | B f y = ran f
20 19 eqeq1d f : B A y | B f y = y ran f = y
21 20 exbidv f : B A y y | B f y = y y ran f = y
22 11 21 syl5bb f : B A ∃! y B f y y ran f = y
23 22 adantl φ f : B A ∃! y B f y y ran f = y
24 10 23 mpbid φ f : B A y ran f = y
25 frn f : B A ran f A
26 25 sseld f : B A y ran f y A
27 vsnid y y
28 eleq2 ran f = y y ran f y y
29 27 28 mpbiri ran f = y y ran f
30 26 29 impel f : B A ran f = y y A
31 30 adantll φ f : B A ran f = y y A
32 ffrn f : B A f : B ran f
33 feq3 ran f = y f : B ran f f : B y
34 32 33 syl5ibcom f : B A ran f = y f : B y
35 34 imp f : B A ran f = y f : B y
36 35 adantll φ f : B A ran f = y f : B y
37 2 ad2antrr φ f : B A ran f = y B W
38 vex y V
39 fsng B W y V f : B y f = B y
40 37 38 39 sylancl φ f : B A ran f = y f : B y f = B y
41 36 40 mpbid φ f : B A ran f = y f = B y
42 31 41 jca φ f : B A ran f = y y A f = B y
43 42 ex φ f : B A ran f = y y A f = B y
44 43 eximdv φ f : B A y ran f = y y y A f = B y
45 24 44 mpd φ f : B A y y A f = B y
46 df-rex y A f = B y y y A f = B y
47 45 46 sylibr φ f : B A y A f = B y
48 47 ex φ f : B A y A f = B y
49 f1osng B W y V B y : B 1-1 onto y
50 2 38 49 sylancl φ B y : B 1-1 onto y
51 50 adantr φ f = B y B y : B 1-1 onto y
52 f1oeq1 f = B y f : B 1-1 onto y B y : B 1-1 onto y
53 52 bicomd f = B y B y : B 1-1 onto y f : B 1-1 onto y
54 53 adantl φ f = B y B y : B 1-1 onto y f : B 1-1 onto y
55 51 54 mpbid φ f = B y f : B 1-1 onto y
56 f1of f : B 1-1 onto y f : B y
57 55 56 syl φ f = B y f : B y
58 57 3adant2 φ y A f = B y f : B y
59 snssi y A y A
60 59 3ad2ant2 φ y A f = B y y A
61 58 60 fssd φ y A f = B y f : B A
62 61 rexlimdv3a φ y A f = B y f : B A
63 48 62 impbid φ f : B A y A f = B y
64 5 63 bitrd φ f A B y A f = B y
65 64 abbi2dv φ A B = f | y A f = B y