Theorem fsn2

Description: A function that maps a singleton to a class is the singleton of an ordered pair. (Contributed by NM, 19-May-2004)

	Ref	Expression
Hypothesis	fsn2.1	$$⊢A\in \mathrm{V}$$
Assertion	fsn2	$$⊢F:\left\{A\right\}⟶B\leftrightarrow \left(F\left(A\right)\in B\wedge F=\left\{⟨A,F\left(A\right)⟩\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsn2.1	$$⊢A\in \mathrm{V}$$
2	1	snid	$$⊢A\in \left\{A\right\}$$
3		ffvelrn	$$⊢\left(F:\left\{A\right\}⟶B\wedge A\in \left\{A\right\}\right)\to F\left(A\right)\in B$$
4	2 3	mpan2	$$⊢F:\left\{A\right\}⟶B\to F\left(A\right)\in B$$
5		ffn	$$⊢F:\left\{A\right\}⟶B\to FFn\left\{A\right\}$$
6		dffn3	$$⊢FFn\left\{A\right\}\leftrightarrow F:\left\{A\right\}⟶\mathrm{ran}F$$
7	6	biimpi	$$⊢FFn\left\{A\right\}\to F:\left\{A\right\}⟶\mathrm{ran}F$$
8		imadmrn	$$⊢F\left[\mathrm{dom}F\right]=\mathrm{ran}F$$
9		fndm	$$⊢FFn\left\{A\right\}\to \mathrm{dom}F=\left\{A\right\}$$
10	9	imaeq2d	$$⊢FFn\left\{A\right\}\to F\left[\mathrm{dom}F\right]=F\left[\left\{A\right\}\right]$$
11	8 10	eqtr3id	$$⊢FFn\left\{A\right\}\to \mathrm{ran}F=F\left[\left\{A\right\}\right]$$
12		fnsnfv	$$⊢\left(FFn\left\{A\right\}\wedge A\in \left\{A\right\}\right)\to \left\{F\left(A\right)\right\}=F\left[\left\{A\right\}\right]$$
13	2 12	mpan2	$$⊢FFn\left\{A\right\}\to \left\{F\left(A\right)\right\}=F\left[\left\{A\right\}\right]$$
14	11 13	eqtr4d	$$⊢FFn\left\{A\right\}\to \mathrm{ran}F=\left\{F\left(A\right)\right\}$$
15	14	feq3d	$$⊢FFn\left\{A\right\}\to \left(F:\left\{A\right\}⟶\mathrm{ran}F\leftrightarrow F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}\right)$$
16	7 15	mpbid	$$⊢FFn\left\{A\right\}\to F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}$$
17	5 16	syl	$$⊢F:\left\{A\right\}⟶B\to F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}$$
18	4 17	jca	$$⊢F:\left\{A\right\}⟶B\to \left(F\left(A\right)\in B\wedge F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}\right)$$
19		snssi	$$⊢F\left(A\right)\in B\to \left\{F\left(A\right)\right\}\subseteq B$$
20		fss	$$⊢\left(F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}\wedge \left\{F\left(A\right)\right\}\subseteq B\right)\to F:\left\{A\right\}⟶B$$
21	20	ancoms	$$⊢\left(\left\{F\left(A\right)\right\}\subseteq B\wedge F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}\right)\to F:\left\{A\right\}⟶B$$
22	19 21	sylan	$$⊢\left(F\left(A\right)\in B\wedge F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}\right)\to F:\left\{A\right\}⟶B$$
23	18 22	impbii	$$⊢F:\left\{A\right\}⟶B\leftrightarrow \left(F\left(A\right)\in B\wedge F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}\right)$$
24		fvex	$$⊢F\left(A\right)\in \mathrm{V}$$
25	1 24	fsn	$$⊢F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}\leftrightarrow F=\left\{⟨A,F\left(A\right)⟩\right\}$$
26	25	anbi2i	$$⊢\left(F\left(A\right)\in B\wedge F:\left\{A\right\}⟶\left\{F\left(A\right)\right\}\right)\leftrightarrow \left(F\left(A\right)\in B\wedge F=\left\{⟨A,F\left(A\right)⟩\right\}\right)$$
27	23 26	bitri	$$⊢F:\left\{A\right\}⟶B\leftrightarrow \left(F\left(A\right)\in B\wedge F=\left\{⟨A,F\left(A\right)⟩\right\}\right)$$