Theorem fsn

Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003)

	Ref	Expression
Hypotheses	fsn.1	|- A e. _V
	fsn.2	|- B e. _V
Assertion	fsn	|- ( F : { A } --> { B } <-> F = { <. A , B >. } )

Proof

Step	Hyp	Ref	Expression
1		fsn.1	|- A e. _V
2		fsn.2	|- B e. _V
3		opelf	|- ( ( F : { A } --> { B } /\ <. x , y >. e. F ) -> ( x e. { A } /\ y e. { B } ) )
4		velsn	|- ( x e. { A } <-> x = A )
5		velsn	|- ( y e. { B } <-> y = B )
6	4 5	anbi12i	|- ( ( x e. { A } /\ y e. { B } ) <-> ( x = A /\ y = B ) )
7	3 6	sylib	|- ( ( F : { A } --> { B } /\ <. x , y >. e. F ) -> ( x = A /\ y = B ) )
8	7	ex	|- ( F : { A } --> { B } -> ( <. x , y >. e. F -> ( x = A /\ y = B ) ) )
9	1	snid	|- A e. { A }
10		feu	|- ( ( F : { A } --> { B } /\ A e. { A } ) -> E! y e. { B } <. A , y >. e. F )
11	9 10	mpan2	|- ( F : { A } --> { B } -> E! y e. { B } <. A , y >. e. F )
12	5	anbi1i	|- ( ( y e. { B } /\ <. A , y >. e. F ) <-> ( y = B /\ <. A , y >. e. F ) )
13		opeq2	|- ( y = B -> <. A , y >. = <. A , B >. )
14	13	eleq1d	|- ( y = B -> ( <. A , y >. e. F <-> <. A , B >. e. F ) )
15	14	pm5.32i	|- ( ( y = B /\ <. A , y >. e. F ) <-> ( y = B /\ <. A , B >. e. F ) )
16	15	biancomi	|- ( ( y = B /\ <. A , y >. e. F ) <-> ( <. A , B >. e. F /\ y = B ) )
17	12 16	bitr2i	|- ( ( <. A , B >. e. F /\ y = B ) <-> ( y e. { B } /\ <. A , y >. e. F ) )
18	17	eubii	|- ( E! y ( <. A , B >. e. F /\ y = B ) <-> E! y ( y e. { B } /\ <. A , y >. e. F ) )
19	2	eueqi	|- E! y y = B
20	19	biantru	|- ( <. A , B >. e. F <-> ( <. A , B >. e. F /\ E! y y = B ) )
21		euanv	|- ( E! y ( <. A , B >. e. F /\ y = B ) <-> ( <. A , B >. e. F /\ E! y y = B ) )
22	20 21	bitr4i	|- ( <. A , B >. e. F <-> E! y ( <. A , B >. e. F /\ y = B ) )
23		df-reu	|- ( E! y e. { B } <. A , y >. e. F <-> E! y ( y e. { B } /\ <. A , y >. e. F ) )
24	18 22 23	3bitr4i	|- ( <. A , B >. e. F <-> E! y e. { B } <. A , y >. e. F )
25	11 24	sylibr	|- ( F : { A } --> { B } -> <. A , B >. e. F )
26		opeq12	|- ( ( x = A /\ y = B ) -> <. x , y >. = <. A , B >. )
27	26	eleq1d	|- ( ( x = A /\ y = B ) -> ( <. x , y >. e. F <-> <. A , B >. e. F ) )
28	25 27	syl5ibrcom	|- ( F : { A } --> { B } -> ( ( x = A /\ y = B ) -> <. x , y >. e. F ) )
29	8 28	impbid	|- ( F : { A } --> { B } -> ( <. x , y >. e. F <-> ( x = A /\ y = B ) ) )
30		opex	|- <. x , y >. e. _V
31	30	elsn	|- ( <. x , y >. e. { <. A , B >. } <-> <. x , y >. = <. A , B >. )
32	1 2	opth2	|- ( <. x , y >. = <. A , B >. <-> ( x = A /\ y = B ) )
33	31 32	bitr2i	|- ( ( x = A /\ y = B ) <-> <. x , y >. e. { <. A , B >. } )
34	29 33	bitrdi	|- ( F : { A } --> { B } -> ( <. x , y >. e. F <-> <. x , y >. e. { <. A , B >. } ) )
35	34	alrimivv	|- ( F : { A } --> { B } -> A. x A. y ( <. x , y >. e. F <-> <. x , y >. e. { <. A , B >. } ) )
36		frel	|- ( F : { A } --> { B } -> Rel F )
37	1 2	relsnop	|- Rel { <. A , B >. }
38		eqrel	|- ( ( Rel F /\ Rel { <. A , B >. } ) -> ( F = { <. A , B >. } <-> A. x A. y ( <. x , y >. e. F <-> <. x , y >. e. { <. A , B >. } ) ) )
39	36 37 38	sylancl	|- ( F : { A } --> { B } -> ( F = { <. A , B >. } <-> A. x A. y ( <. x , y >. e. F <-> <. x , y >. e. { <. A , B >. } ) ) )
40	35 39	mpbird	|- ( F : { A } --> { B } -> F = { <. A , B >. } )
41	1 2	f1osn	|- { <. A , B >. } : { A } -1-1-onto-> { B }
42		f1oeq1	|- ( F = { <. A , B >. } -> ( F : { A } -1-1-onto-> { B } <-> { <. A , B >. } : { A } -1-1-onto-> { B } ) )
43	41 42	mpbiri	|- ( F = { <. A , B >. } -> F : { A } -1-1-onto-> { B } )
44		f1of	|- ( F : { A } -1-1-onto-> { B } -> F : { A } --> { B } )
45	43 44	syl	|- ( F = { <. A , B >. } -> F : { A } --> { B } )
46	40 45	impbii	|- ( F : { A } --> { B } <-> F = { <. A , B >. } )