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

Metamath Proof Explorer

Theorem fsn

Proof