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 \in V$
	fsn.2	$⊢ B \in V$
Assertion	fsn	$⊢ F : \{A\} ⟶ \{B\} \leftrightarrow F = \{⟨A, B⟩\}$

Proof

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

Metamath Proof Explorer

Theorem fsn

Proof