Theorem mapsnd 6914

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 4289	. . . . 5 |- ( B e. W -> { B } e. _V )
4	2, 3	syl 14	. . . 4 |- ( ph -> { B } e. _V )
5	1, 4	elmapd 6887	. . 3 |- ( ph -> ( f e. ( A ^m { B } ) <-> f : { B } --> A ) )
6		ffn 5499	. . . . . . . . 9 |- ( f : { B } --> A -> f Fn { B } )
7		snidg 3711	. . . . . . . . . 10 |- ( B e. W -> B e. { B } )
8	2, 7	syl 14	. . . . . . . . 9 |- ( ph -> B e. { B } )
9		fneu 5453	. . . . . . . . 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 3754	. . . . . . . . 9 |- ( E! y B f y <-> E. y { y | B f y } = { y } )
12		imasng 5118	. . . . . . . . . . . . 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 5505	. . . . . . . . . . . . . 14 |- ( f : { B } --> A -> dom f = { B } )
15	14	imaeq2d 5092	. . . . . . . . . . . . 13 |- ( f : { B } --> A -> ( f " dom f ) = ( f " { B } ) )
16		imadmrn 5102	. . . . . . . . . . . . 13 |- ( f " dom f ) = ran f
17	15, 16	eqtr3di 2280	. . . . . . . . . . . 12 |- ( f : { B } --> A -> ( f " { B } ) = ran f )
18	13, 17	sylan9req 2286	. . . . . . . . . . 11 |- ( ( ph /\ f : { B } --> A ) -> { y | B f y } = ran f )
19	18	eqeq1d 2241	. . . . . . . . . 10 |- ( ( ph /\ f : { B } --> A ) -> ( { y | B f y } = { y } <-> ran f = { y } ) )
20	19	exbidv 1874	. . . . . . . . 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 5508	. . . . . . . . . . . . 13 |- ( f : { B } --> A -> ran f C_ A )
24	23	sseld 3236	. . . . . . . . . . . 12 |- ( f : { B } --> A -> ( y e. ran f -> y e. A ) )
25		vsnid 3714	. . . . . . . . . . . . 13 |- y e. { y }
26		eleq2 2296	. . . . . . . . . . . . 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 476	. . . . . . . . . 10 |- ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> y e. A )
30		ffrn 5511	. . . . . . . . . . . . . 14 |- ( f : { B } --> A -> f : { B } --> ran f )
31		feq3 5484	. . . . . . . . . . . . . 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 476	. . . . . . . . . . 11 |- ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> f : { B } --> { y } )
35	2	ad2antrr 488	. . . . . . . . . . . 12 |- ( ( ( ph /\ f : { B } --> A ) /\ ran f = { y } ) -> B e. W )
36		vex 2815	. . . . . . . . . . . 12 |- y e. _V
37		fsng 5841	. . . . . . . . . . . 12 |- ( ( B e. W /\ y e. _V ) -> ( f : { B } --> { y } <-> f = { <. B , y >. } ) )
38	35, 36, 37	sylancl 413	. . . . . . . . . . 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 1929	. . . . . . 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 2526	. . . . . 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 5648	. . . . . . . . . . 11 |- ( ( B e. W /\ y e. _V ) -> { <. B , y >. } : { B } -1-1-onto-> { y } )
48	2, 36, 47	sylancl 413	. . . . . . . . . 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 5593	. . . . . . . . . . 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 5605	. . . . . . . 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 1043	. . . . . 6 |- ( ( ph /\ y e. A /\ f = { <. B , y >. } ) -> f : { B } --> { y } )
57		snssi 3831	. . . . . . 7 |- ( y e. A -> { y } C_ A )
58	57	3ad2ant2 1046	. . . . . 6 |- ( ( ph /\ y e. A /\ f = { <. B , y >. } ) -> { y } C_ A )
59	56, 58	fssd 5513	. . . . 5 |- ( ( ph /\ y e. A /\ f = { <. B , y >. } ) -> f : { B } --> A )
60	59	rexlimdv3a 2662	. . . 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 2363	1 |- ( ph -> ( A ^m { B } ) = { f | E. y e. A f = { <. B , y >. } } )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1005   = wceq 1398   E.wex 1541   E!weu 2080   e. wcel 2203   {cab 2218   E.wrex 2521   _Vcvv 2812   C_ wss 3210   {csn 3682   <.cop 3685   class class class wbr 4102   dom cdm 4740   ran crn 4741   "cima 4743   Fn wfn 5338   -->wf 5339   -1-1-onto->wf1o 5342  (class class class)co 6041   ^m cmap 6873

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4221  ax-pow 4279  ax-pr 4314  ax-un 4545  ax-setind 4650

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-ral 2525  df-rex 2526  df-reu 2527  df-v 2814  df-sbc 3042  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-pw 3667  df-sn 3688  df-pr 3689  df-op 3691  df-uni 3908  df-br 4103  df-opab 4165  df-id 4405  df-xp 4746  df-rel 4747  df-cnv 4748  df-co 4749  df-dm 4750  df-rn 4751  df-res 4752  df-ima 4753  df-iota 5303  df-fun 5345  df-fn 5346  df-f 5347  df-f1 5348  df-fo 5349  df-f1o 5350  df-fv 5351  df-ov 6044  df-oprab 6045  df-mpo 6046  df-map 6875

This theorem is referenced by:  mapsnend  7043