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 V$
	funopsn.y	$⊢ Y \in V$
Assertion	funop	$⊢ Fun ⟨X, Y⟩ \leftrightarrow \exists a (X = \{a\} \land ⟨X, Y⟩ = \{⟨a, a⟩\})$

Proof

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

Metamath Proof Explorer

Theorem funop

Proof