funopsn

Description: If a function is an ordered pair then it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) (Proof shortened by AV, 15-Jul-2021) (Proof shortened by Eric Schmidt, 9-May-2026) 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	funopsn	$⊢ (Fun F \land F = ⟨X, Y⟩) \to \exists a (X = \{a\} \land F = \{⟨a, a⟩\})$

Proof

Step	Hyp	Ref	Expression
1		funopsn.x	$⊢ X \in V$
2		funopsn.y	$⊢ Y \in V$
3		funiun	$⊢ Fun F \to F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}$
4		eqeq1	$⊢ F = ⟨X, Y⟩ \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \leftrightarrow ⟨X, Y⟩ = ⋃_{x \in dom F} \{⟨x, F (x)⟩\})$
5		eqcom	$⊢ ⟨X, Y⟩ = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \leftrightarrow ⋃_{x \in dom F} \{⟨x, F (x)⟩\} = ⟨X, Y⟩$
6	4 5	bitrdi	$⊢ F = ⟨X, Y⟩ \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \leftrightarrow ⋃_{x \in dom F} \{⟨x, F (x)⟩\} = ⟨X, Y⟩)$
7		fvex	$⊢ F (x) \in V$
8	7 1 2	iunopeqop	$⊢ ⋃_{x \in dom F} \{⟨x, F (x)⟩\} = ⟨X, Y⟩ \to \exists a dom F = \{a\}$
9	6 8	biimtrdi	$⊢ F = ⟨X, Y⟩ \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \to \exists a dom F = \{a\})$
10	9	imp	$⊢ (F = ⟨X, Y⟩ \land F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}) \to \exists a dom F = \{a\}$
11		iuneq1	$⊢ dom F = \{a\} \to ⋃_{x \in dom F} \{⟨x, F (x)⟩\} = ⋃_{x \in \{a\}} \{⟨x, F (x)⟩\}$
12		vex	$⊢ a \in V$
13		id	$⊢ x = a \to x = a$
14		fveq2	$⊢ x = a \to F (x) = F (a)$
15	13 14	opeq12d	$⊢ x = a \to ⟨x, F (x)⟩ = ⟨a, F (a)⟩$
16	15	sneqd	$⊢ x = a \to \{⟨x, F (x)⟩\} = \{⟨a, F (a)⟩\}$
17	12 16	iunxsn	$⊢ ⋃_{x \in \{a\}} \{⟨x, F (x)⟩\} = \{⟨a, F (a)⟩\}$
18	11 17	eqtrdi	$⊢ dom F = \{a\} \to ⋃_{x \in dom F} \{⟨x, F (x)⟩\} = \{⟨a, F (a)⟩\}$
19	18	eqeq2d	$⊢ dom F = \{a\} \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \leftrightarrow F = \{⟨a, F (a)⟩\})$
20	19	adantl	$⊢ (F = ⟨X, Y⟩ \land dom F = \{a\}) \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \leftrightarrow F = \{⟨a, F (a)⟩\})$
21		eqeq1	$⊢ F = ⟨X, Y⟩ \to (F = \{⟨a, F (a)⟩\} \leftrightarrow ⟨X, Y⟩ = \{⟨a, F (a)⟩\})$
22		eqcom	$⊢ ⟨X, Y⟩ = \{⟨a, F (a)⟩\} \leftrightarrow \{⟨a, F (a)⟩\} = ⟨X, Y⟩$
23		fvex	$⊢ F (a) \in V$
24	12 23	snopeqop	$⊢ \{⟨a, F (a)⟩\} = ⟨X, Y⟩ \leftrightarrow (a = F (a) \land X = Y \land X = \{a\})$
25	22 24	sylbb	$⊢ ⟨X, Y⟩ = \{⟨a, F (a)⟩\} \to (a = F (a) \land X = Y \land X = \{a\})$
26	21 25	biimtrdi	$⊢ F = ⟨X, Y⟩ \to (F = \{⟨a, F (a)⟩\} \to (a = F (a) \land X = Y \land X = \{a\}))$
27		simpr3	$⊢ (F = \{⟨a, F (a)⟩\} \land (a = F (a) \land X = Y \land X = \{a\})) \to X = \{a\}$
28		simp1	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to a = F (a)$
29	28	eqcomd	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to F (a) = a$
30	29	opeq2d	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to ⟨a, F (a)⟩ = ⟨a, a⟩$
31	30	sneqd	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to \{⟨a, F (a)⟩\} = \{⟨a, a⟩\}$
32	31	eqeq2d	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to (F = \{⟨a, F (a)⟩\} \leftrightarrow F = \{⟨a, a⟩\})$
33	32	biimpac	$⊢ (F = \{⟨a, F (a)⟩\} \land (a = F (a) \land X = Y \land X = \{a\})) \to F = \{⟨a, a⟩\}$
34	27 33	jca	$⊢ (F = \{⟨a, F (a)⟩\} \land (a = F (a) \land X = Y \land X = \{a\})) \to (X = \{a\} \land F = \{⟨a, a⟩\})$
35	34	ex	$⊢ F = \{⟨a, F (a)⟩\} \to ((a = F (a) \land X = Y \land X = \{a\}) \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
36	26 35	sylcom	$⊢ F = ⟨X, Y⟩ \to (F = \{⟨a, F (a)⟩\} \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
37	36	adantr	$⊢ (F = ⟨X, Y⟩ \land dom F = \{a\}) \to (F = \{⟨a, F (a)⟩\} \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
38	20 37	sylbid	$⊢ (F = ⟨X, Y⟩ \land dom F = \{a\}) \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
39	38	impancom	$⊢ (F = ⟨X, Y⟩ \land F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}) \to (dom F = \{a\} \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
40	39	eximdv	$⊢ (F = ⟨X, Y⟩ \land F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}) \to (\exists a dom F = \{a\} \to \exists a (X = \{a\} \land F = \{⟨a, a⟩\}))$
41	10 40	mpd	$⊢ (F = ⟨X, Y⟩ \land F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}) \to \exists a (X = \{a\} \land F = \{⟨a, a⟩\})$
42	3 41	sylan2	$⊢ (F = ⟨X, Y⟩ \land Fun F) \to \exists a (X = \{a\} \land F = \{⟨a, a⟩\})$
43	42	ancoms	$⊢ (Fun F \land F = ⟨X, Y⟩) \to \exists a (X = \{a\} \land F = \{⟨a, a⟩\})$

Metamath Proof Explorer

Theorem funopsn

Proof