Theorem funop

Description: An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng , as relsnopg is to relop . (New usage is discouraged.)

	Ref	Expression
Hypotheses	funopsn.x	$$⊢X\in \mathrm{V}$$
	funopsn.y	$$⊢Y\in \mathrm{V}$$
Assertion	funop	$$⊢\mathrm{Fun}⟨X,Y⟩\leftrightarrow \exists a\left(X=\left\{a\right\}\wedge ⟨X,Y⟩=\left\{⟨a,a⟩\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		funopsn.x	$$⊢X\in \mathrm{V}$$
2		funopsn.y	$$⊢Y\in \mathrm{V}$$
3		eqid	$$⊢⟨X,Y⟩=⟨X,Y⟩$$
4	1 2	funopsn	$$⊢\left(\mathrm{Fun}⟨X,Y⟩\wedge ⟨X,Y⟩=⟨X,Y⟩\right)\to \exists a\left(X=\left\{a\right\}\wedge ⟨X,Y⟩=\left\{⟨a,a⟩\right\}\right)$$
5	3 4	mpan2	$$⊢\mathrm{Fun}⟨X,Y⟩\to \exists a\left(X=\left\{a\right\}\wedge ⟨X,Y⟩=\left\{⟨a,a⟩\right\}\right)$$
6		vex	$$⊢a\in \mathrm{V}$$
7	6 6	funsn	$$⊢\mathrm{Fun}\left\{⟨a,a⟩\right\}$$
8		funeq	$$⊢⟨X,Y⟩=\left\{⟨a,a⟩\right\}\to \left(\mathrm{Fun}⟨X,Y⟩\leftrightarrow \mathrm{Fun}\left\{⟨a,a⟩\right\}\right)$$
9	7 8	mpbiri	$$⊢⟨X,Y⟩=\left\{⟨a,a⟩\right\}\to \mathrm{Fun}⟨X,Y⟩$$
10	9	adantl	$$⊢\left(X=\left\{a\right\}\wedge ⟨X,Y⟩=\left\{⟨a,a⟩\right\}\right)\to \mathrm{Fun}⟨X,Y⟩$$
11	10	exlimiv	$$⊢\exists a\left(X=\left\{a\right\}\wedge ⟨X,Y⟩=\left\{⟨a,a⟩\right\}\right)\to \mathrm{Fun}⟨X,Y⟩$$
12	5 11	impbii	$$⊢\mathrm{Fun}⟨X,Y⟩\leftrightarrow \exists a\left(X=\left\{a\right\}\wedge ⟨X,Y⟩=\left\{⟨a,a⟩\right\}\right)$$