Theorem mapsnd 6963

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.)

Hypotheses

Ref	Expression
mapsnd.1	|- ( ph -> A e. V )
mapsnd.2	|- ( ph -> B e. W )

Assertion

Ref	Expression
mapsnd	|- ( ph -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } )

Distinct variable groups:   A, f, y   B, f, y   ph, f, y

Allowed substitution hints:   V( y, f)   W( y, f)

Proof of Theorem mapsnd

Step	Hyp	Ref	Expression
1		mapsnd.1	. . . 4 |- ( ph -> A e. V )
2		mapsnd.2	. . . . 5 |- ( ph -> B e. W )
3		snexg 4319	. . . . 5 |- ( B e. W -> { B } e. _V )
4	2, 3	syl 14	. . . 4 |- ( ph -> { B } e. _V )
5	1, 4	elmapd 6929	. . 3 |- ( ph -> ( f e. ( A ^m { B } ) <-> f : { B } --> A ) )
6		ffn 5531	. . . . . . . . 9 |- ( f : { B } --> A -> f Fn { B } )
7		snidg 3737	. . . . . . . . . 10 |- ( B e. W -> B e. { B } )
8	2, 7	syl 14	. . . . . . . . 9 |- ( ph -> B e. { B } )
9		fneu 5485	. . . . . . . . 9 |- ( ( f Fn { B } /\ B e. { B } ) -> E! y B f y )
10	6, 8, 9	syl2anr 290	. . . . . . . 8 |- ( ( ph /\ f : { B } --> A ) -> E! y B f y )
11		euabsn 3780	. . . . . . . . 9 |- ( E! y B f y <-> E. y { y | B f y } = { y } )
12		imasng 5150	. . . . . . . . . . . . 13 |- ( B e. W -> ( f " { B } ) = { y | B f y } )
13	2, 12	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( f " { B } ) = { y | B f y } )
14		fdm 5537	. . . . . . . . . . . . . 14 |- ( f : { B } --> A -> dom f = { B } )
15	14	imaeq2d 5124	. . . . . . . . . . . . 13 |- ( f : { B } --> A -> ( f " dom f ) = ( f " { B } ) )
16		imadmrn 5134	. . . . . . . . . . . . 13 |- ( f " dom f ) = ran f
17	15, 16	eqtr3di 2286	. . . . . . . . . . . 12 |- ( f : { B } --> A -> ( f " { B } ) = ran f )
18	13, 17	sylan9req 2292	. . . . . . . . . . 11 |- ( ( ph /\ f : { B } --> A ) -> { y | B f y } = ran f )
19	18	eqeq1d 2247	. . . . . . . . . 10 |- ( ( ph /\ f : { B } --> A ) -> ( { y | B f y } = { y } <-> ran f = { y } ) )
20	19	exbidv 1878	. . . . . . . . 9 |- ( ( ph /\ f : { B } --> A ) -> ( E. y { y | B f y } = { y } <-> E. y ran f = { y } ) )
21	11, 20	bitrid 192	. . . . . . . 8 |- ( ( ph /\ f : { B } --> A ) -> ( E! y B f y <-> E. y ran f = { y } ) )
22	10, 21	mpbid 147	. . . . . . 7 |- ( ( ph /\ f : { B } --> A ) -> E. y ran f = { y } )
23		frn 5540	. . . . . . . . . . . . 13 |- ( f : { B } --> A -> ran f C_ A )
24	23	sseld 3247	. . . . . . . . . . . 12 |- ( f : { B } --> A -> ( y e. ran f -> y e. A ) )
25		vsnid 3740	. . . . . . . . . . . . 13 |- y e. { y }
26		eleq2 2302	. . . . . . . . . . . . 13 |- ( ran f = { y } -> ( y e. ran f <-> y e. { y } ) )
27	25, 26	mpbiri 168	. . . . . . . . . . . 12 |- ( ran f = { y } -> y e. ran f )
28	24, 27	impel 280	. . . . . . . . . . 11 |- ( ( f : { B } --> A /\ ran f = { y } ) -> y e. A )
29	28	adantll 480	. . . . . . . . . 10 |- ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> y e. A )
30		ffrn 5543	. . . . . . . . . . . . . 14 |- ( f : { B } --> A -> f : { B } --> ran f )
31		feq3 5516	. . . . . . . . . . . . . 14 |- ( ran f = { y } -> ( f : { B } --> ran f <-> f : { B } --> { y } ) )
32	30, 31	syl5ibcom 155	. . . . . . . . . . . . 13 |- ( f : { B } --> A -> ( ran f = { y } -> f : { B } --> { y } ) )
33	32	imp 124	. . . . . . . . . . . 12 |- ( ( f : { B } --> A /\ ran f = { y } ) -> f : { B } --> { y } )
34	33	adantll 480	. . . . . . . . . . 11 |- ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> f : { B } --> { y } )
35	2	ad2antrr 492	. . . . . . . . . . . 12 |- ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> B e. W )
36		vex 2824	. . . . . . . . . . . 12 |- y e. _V
37		fsng 5875	. . . . . . . . . . . 12 |- ( ( B e. W /\ y e. _V ) -> ( f : { B } --> { y } <-> f = { <. B , y >. } ) )
38	35, 36, 37	sylancl 417	. . . . . . . . . . 11 |- ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> ( f : { B } --> { y } <-> f = { <. B , y >. } ) )
39	34, 38	mpbid 147	. . . . . . . . . 10 |- ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> f = { <. B , y >. } )
40	29, 39	jca 306	. . . . . . . . 9 |- ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> ( y e. A /\ f = { <. B , y >. } ) )
41	40	ex 115	. . . . . . . 8 |- ( ( ph /\ f : { B } --> A ) -> ( ran f = { y } -> ( y e. A /\ f = { <. B , y >. } ) ) )
42	41	eximdv 1933	. . . . . . 7 |- ( ( ph /\ f : { B } --> A ) -> ( E. y ran f = { y } -> E. y ( y e. A /\ f = { <. B , y >. } ) ) )
43	22, 42	mpd 13	. . . . . 6 |- ( ( ph /\ f : { B } --> A ) -> E. y ( y e. A /\ f = { <. B , y >. } ) )
44		df-rex 2534	. . . . . 6 |- ( E. y e. A f = { <. B , y >. } <-> E. y ( y e. A /\ f = { <. B , y >. } ) )
45	43, 44	sylibr 134	. . . . 5 |- ( ( ph /\ f : { B } --> A ) -> E. y e. A f = { <. B , y >. } )
46	45	ex 115	. . . 4 |- ( ph -> ( f : { B } --> A -> E. y e. A f = { <. B , y >. } ) )
47		f1osng 5680	. . . . . . . . . . 11 |- ( ( B e. W /\ y e. _V ) -> { <. B , y >. } : { B } -1-1-onto-> { y } )
48	2, 36, 47	sylancl 417	. . . . . . . . . 10 |- ( ph -> { <. B , y >. } : { B } -1-1-onto-> { y } )
49	48	adantr 276	. . . . . . . . 9 |- ( ( ph /\ f = { <. B , y >. } ) -> { <. B , y >. } : { B } -1-1-onto-> { y } )
50		f1oeq1 5625	. . . . . . . . . . 11 |- ( f = { <. B , y >. } -> ( f : { B } -1-1-onto-> { y } <-> { <. B , y >. } : { B } -1-1-onto-> { y } ) )
51	50	bicomd 141	. . . . . . . . . 10 |- ( f = { <. B , y >. } -> ( { <. B , y >. } : { B } -1-1-onto-> { y } <-> f : { B } -1-1-onto-> { y } ) )
52	51	adantl 277	. . . . . . . . 9 |- ( ( ph /\ f = { <. B , y >. } ) -> ( { <. B , y >. } : { B } -1-1-onto-> { y } <-> f : { B } -1-1-onto-> { y } ) )
53	49, 52	mpbid 147	. . . . . . . 8 |- ( ( ph /\ f = { <. B , y >. } ) -> f : { B } -1-1-onto-> { y } )
54		f1of 5637	. . . . . . . 8 |- ( f : { B } -1-1-onto-> { y } -> f : { B } --> { y } )
55	53, 54	syl 14	. . . . . . 7 |- ( ( ph /\ f = { <. B , y >. } ) -> f : { B } --> { y } )
56	55	3adant2 1047	. . . . . 6 |- ( ( ph /\ y e. A /\ f = { <. B , y >. } ) -> f : { B } --> { y } )
57		snssi 3857	. . . . . . 7 |- ( y e. A -> { y } C_ A )
58	57	3ad2ant2 1050	. . . . . 6 |- ( ( ph /\ y e. A /\ f = { <. B , y >. } ) -> { y } C_ A )
59	56, 58	fssd 5545	. . . . 5 |- ( ( ph /\ y e. A /\ f = { <. B , y >. } ) -> f : { B } --> A )
60	59	rexlimdv3a 2670	. . . 4 |- ( ph -> ( E. y e. A f = { <. B , y >. } -> f : { B } --> A ) )
61	46, 60	impbid 129	. . 3 |- ( ph -> ( f : { B } --> A <-> E. y e. A f = { <. B , y >. } ) )
62	5, 61	bitrd 188	. 2 |- ( ph -> ( f e. ( A ^m { B } ) <-> E. y e. A f = { <. B , y >. } ) )
63	62	eqabdv 2369	1 |- ( ph -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1009   = wceq 1402   E.wex 1545   E!weu 2086   e. wcel 2209   {cab 2224   E.wrex 2529   _Vcvv 2821   C_ wss 3220   {csn 3708   <.cop 3711   class class class wbr 4128   dom cdm 4772   ran crn 4773   "cima 4775   Fn wfn 5370   -->wf 5371   -1-1-onto->wf1o 5374  (class class class)co 6078   ^m cmap 6915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344  ax-un 4576  ax-setind 4682

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382  df-fv 5383  df-ov 6081  df-oprab 6082  df-mpo 6083  df-map 6917

This theorem is referenced by:  mapsnend  7092