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) 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	6	adantl	$⊢ (Fun F \land F = ⟨X, Y⟩) \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \leftrightarrow ⋃_{x \in dom F} \{⟨x, F (x)⟩\} = ⟨X, Y⟩)$
8	1 2	opnzi	$⊢ ⟨X, Y⟩ \neq \emptyset$
9		neeq1	$⊢ ⟨X, Y⟩ = F \to (⟨X, Y⟩ \neq \emptyset \leftrightarrow F \neq \emptyset)$
10	9	eqcoms	$⊢ F = ⟨X, Y⟩ \to (⟨X, Y⟩ \neq \emptyset \leftrightarrow F \neq \emptyset)$
11		funrel	$⊢ Fun F \to Rel F$
12		reldm0	$⊢ Rel F \to (F = \emptyset \leftrightarrow dom F = \emptyset)$
13	11 12	syl	$⊢ Fun F \to (F = \emptyset \leftrightarrow dom F = \emptyset)$
14	13	biimprd	$⊢ Fun F \to (dom F = \emptyset \to F = \emptyset)$
15	14	necon3d	$⊢ Fun F \to (F \neq \emptyset \to dom F \neq \emptyset)$
16	15	com12	$⊢ F \neq \emptyset \to (Fun F \to dom F \neq \emptyset)$
17	10 16	biimtrdi	$⊢ F = ⟨X, Y⟩ \to (⟨X, Y⟩ \neq \emptyset \to (Fun F \to dom F \neq \emptyset))$
18	17	com3l	$⊢ ⟨X, Y⟩ \neq \emptyset \to (Fun F \to (F = ⟨X, Y⟩ \to dom F \neq \emptyset))$
19	18	impd	$⊢ ⟨X, Y⟩ \neq \emptyset \to ((Fun F \land F = ⟨X, Y⟩) \to dom F \neq \emptyset)$
20	8 19	ax-mp	$⊢ (Fun F \land F = ⟨X, Y⟩) \to dom F \neq \emptyset$
21		fvex	$⊢ F (x) \in V$
22	21 1 2	iunopeqop	$⊢ dom F \neq \emptyset \to (⋃_{x \in dom F} \{⟨x, F (x)⟩\} = ⟨X, Y⟩ \to \exists a dom F = \{a\})$
23	20 22	syl	$⊢ (Fun F \land F = ⟨X, Y⟩) \to (⋃_{x \in dom F} \{⟨x, F (x)⟩\} = ⟨X, Y⟩ \to \exists a dom F = \{a\})$
24	7 23	sylbid	$⊢ (Fun F \land F = ⟨X, Y⟩) \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \to \exists a dom F = \{a\})$
25	24	imp	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}) \to \exists a dom F = \{a\}$
26		iuneq1	$⊢ dom F = \{a\} \to ⋃_{x \in dom F} \{⟨x, F (x)⟩\} = ⋃_{x \in \{a\}} \{⟨x, F (x)⟩\}$
27		vex	$⊢ a \in V$
28		id	$⊢ x = a \to x = a$
29		fveq2	$⊢ x = a \to F (x) = F (a)$
30	28 29	opeq12d	$⊢ x = a \to ⟨x, F (x)⟩ = ⟨a, F (a)⟩$
31	30	sneqd	$⊢ x = a \to \{⟨x, F (x)⟩\} = \{⟨a, F (a)⟩\}$
32	27 31	iunxsn	$⊢ ⋃_{x \in \{a\}} \{⟨x, F (x)⟩\} = \{⟨a, F (a)⟩\}$
33	26 32	eqtrdi	$⊢ dom F = \{a\} \to ⋃_{x \in dom F} \{⟨x, F (x)⟩\} = \{⟨a, F (a)⟩\}$
34	33	adantl	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land dom F = \{a\}) \to ⋃_{x \in dom F} \{⟨x, F (x)⟩\} = \{⟨a, F (a)⟩\}$
35	34	eqeq2d	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land dom F = \{a\}) \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \leftrightarrow F = \{⟨a, F (a)⟩\})$
36		eqeq1	$⊢ F = ⟨X, Y⟩ \to (F = \{⟨a, F (a)⟩\} \leftrightarrow ⟨X, Y⟩ = \{⟨a, F (a)⟩\})$
37	36	adantl	$⊢ (Fun F \land F = ⟨X, Y⟩) \to (F = \{⟨a, F (a)⟩\} \leftrightarrow ⟨X, Y⟩ = \{⟨a, F (a)⟩\})$
38		eqcom	$⊢ ⟨X, Y⟩ = \{⟨a, F (a)⟩\} \leftrightarrow \{⟨a, F (a)⟩\} = ⟨X, Y⟩$
39		fvex	$⊢ F (a) \in V$
40	27 39	snopeqop	$⊢ \{⟨a, F (a)⟩\} = ⟨X, Y⟩ \leftrightarrow (a = F (a) \land X = Y \land X = \{a\})$
41	38 40	sylbb	$⊢ ⟨X, Y⟩ = \{⟨a, F (a)⟩\} \to (a = F (a) \land X = Y \land X = \{a\})$
42	37 41	biimtrdi	$⊢ (Fun F \land F = ⟨X, Y⟩) \to (F = \{⟨a, F (a)⟩\} \to (a = F (a) \land X = Y \land X = \{a\}))$
43	42	imp	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land F = \{⟨a, F (a)⟩\}) \to (a = F (a) \land X = Y \land X = \{a\})$
44		simpr3	$⊢ (F = \{⟨a, F (a)⟩\} \land (a = F (a) \land X = Y \land X = \{a\})) \to X = \{a\}$
45		simp1	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to a = F (a)$
46	45	eqcomd	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to F (a) = a$
47	46	opeq2d	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to ⟨a, F (a)⟩ = ⟨a, a⟩$
48	47	sneqd	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to \{⟨a, F (a)⟩\} = \{⟨a, a⟩\}$
49	48	eqeq2d	$⊢ (a = F (a) \land X = Y \land X = \{a\}) \to (F = \{⟨a, F (a)⟩\} \leftrightarrow F = \{⟨a, a⟩\})$
50	49	biimpac	$⊢ (F = \{⟨a, F (a)⟩\} \land (a = F (a) \land X = Y \land X = \{a\})) \to F = \{⟨a, a⟩\}$
51	44 50	jca	$⊢ (F = \{⟨a, F (a)⟩\} \land (a = F (a) \land X = Y \land X = \{a\})) \to (X = \{a\} \land F = \{⟨a, a⟩\})$
52	51	ex	$⊢ F = \{⟨a, F (a)⟩\} \to ((a = F (a) \land X = Y \land X = \{a\}) \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
53	52	adantl	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land F = \{⟨a, F (a)⟩\}) \to ((a = F (a) \land X = Y \land X = \{a\}) \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
54	53	a1dd	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land F = \{⟨a, F (a)⟩\}) \to ((a = F (a) \land X = Y \land X = \{a\}) \to (dom F = \{a\} \to (X = \{a\} \land F = \{⟨a, a⟩\})))$
55	43 54	mpd	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land F = \{⟨a, F (a)⟩\}) \to (dom F = \{a\} \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
56	55	impancom	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land dom F = \{a\}) \to (F = \{⟨a, F (a)⟩\} \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
57	35 56	sylbid	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land dom F = \{a\}) \to (F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\} \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
58	57	impancom	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}) \to (dom F = \{a\} \to (X = \{a\} \land F = \{⟨a, a⟩\}))$
59	58	eximdv	$⊢ ((Fun F \land 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⟩\}))$
60	25 59	mpd	$⊢ ((Fun F \land F = ⟨X, Y⟩) \land F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}) \to \exists a (X = \{a\} \land F = \{⟨a, a⟩\})$
61	3 60	mpidan	$⊢ (Fun F \land F = ⟨X, Y⟩) \to \exists a (X = \{a\} \land F = \{⟨a, a⟩\})$

Metamath Proof Explorer

Theorem funopsn

Proof