funopg

Description: A Kuratowski ordered pair of sets is a function only if its components are equal. (Contributed by NM, 5-Jun-2008) (Revised by Mario Carneiro, 26-Apr-2015) 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
	Assertion	funopg	$⊢ (A \in V \land B \in W \land Fun ⟨A, B⟩) \to A = B$

Proof

Step	Hyp	Ref	Expression
1		opeq1	$⊢ u = A \to ⟨u, t⟩ = ⟨A, t⟩$
2	1	funeqd	$⊢ u = A \to (Fun ⟨u, t⟩ \leftrightarrow Fun ⟨A, t⟩)$
3		eqeq1	$⊢ u = A \to (u = t \leftrightarrow A = t)$
4	2 3	imbi12d	$⊢ u = A \to ((Fun ⟨u, t⟩ \to u = t) \leftrightarrow (Fun ⟨A, t⟩ \to A = t))$
5		opeq2	$⊢ t = B \to ⟨A, t⟩ = ⟨A, B⟩$
6	5	funeqd	$⊢ t = B \to (Fun ⟨A, t⟩ \leftrightarrow Fun ⟨A, B⟩)$
7		eqeq2	$⊢ t = B \to (A = t \leftrightarrow A = B)$
8	6 7	imbi12d	$⊢ t = B \to ((Fun ⟨A, t⟩ \to A = t) \leftrightarrow (Fun ⟨A, B⟩ \to A = B))$
9		funrel	$⊢ Fun ⟨u, t⟩ \to Rel ⟨u, t⟩$
10		vex	$⊢ u \in V$
11		vex	$⊢ t \in V$
12	10 11	relop	$⊢ Rel ⟨u, t⟩ \leftrightarrow \exists x \exists y (u = \{x\} \land t = \{x, y\})$
13	9 12	sylib	$⊢ Fun ⟨u, t⟩ \to \exists x \exists y (u = \{x\} \land t = \{x, y\})$
14	10 11	opth	$⊢ ⟨u, t⟩ = ⟨\{x\}, \{x, y\}⟩ \leftrightarrow (u = \{x\} \land t = \{x, y\})$
15		vex	$⊢ x \in V$
16	15	opid	$⊢ ⟨x, x⟩ = \{\{x\}\}$
17	16	preq1i	$⊢ \{⟨x, x⟩, \{\{x\}, \{x, y\}\}\} = \{\{\{x\}\}, \{\{x\}, \{x, y\}\}\}$
18		vex	$⊢ y \in V$
19	15 18	dfop	$⊢ ⟨x, y⟩ = \{\{x\}, \{x, y\}\}$
20	19	preq2i	$⊢ \{⟨x, x⟩, ⟨x, y⟩\} = \{⟨x, x⟩, \{\{x\}, \{x, y\}\}\}$
21		snex	$⊢ \{x\} \in V$
22		zfpair2	$⊢ \{x, y\} \in V$
23	21 22	dfop	$⊢ ⟨\{x\}, \{x, y\}⟩ = \{\{\{x\}\}, \{\{x\}, \{x, y\}\}\}$
24	17 20 23	3eqtr4ri	$⊢ ⟨\{x\}, \{x, y\}⟩ = \{⟨x, x⟩, ⟨x, y⟩\}$
25	24	eqeq2i	$⊢ ⟨u, t⟩ = ⟨\{x\}, \{x, y\}⟩ \leftrightarrow ⟨u, t⟩ = \{⟨x, x⟩, ⟨x, y⟩\}$
26	14 25	bitr3i	$⊢ (u = \{x\} \land t = \{x, y\}) \leftrightarrow ⟨u, t⟩ = \{⟨x, x⟩, ⟨x, y⟩\}$
27		dffun4	$⊢ Fun ⟨u, t⟩ \leftrightarrow (Rel ⟨u, t⟩ \land \forall z \forall w \forall v ((⟨z, w⟩ \in ⟨u, t⟩ \land ⟨z, v⟩ \in ⟨u, t⟩) \to w = v))$
28	27	simprbi	$⊢ Fun ⟨u, t⟩ \to \forall z \forall w \forall v ((⟨z, w⟩ \in ⟨u, t⟩ \land ⟨z, v⟩ \in ⟨u, t⟩) \to w = v)$
29		opex	$⊢ ⟨x, x⟩ \in V$
30	29	prid1	$⊢ ⟨x, x⟩ \in \{⟨x, x⟩, ⟨x, y⟩\}$
31		eleq2	$⊢ ⟨u, t⟩ = \{⟨x, x⟩, ⟨x, y⟩\} \to (⟨x, x⟩ \in ⟨u, t⟩ \leftrightarrow ⟨x, x⟩ \in \{⟨x, x⟩, ⟨x, y⟩\})$
32	30 31	mpbiri	$⊢ ⟨u, t⟩ = \{⟨x, x⟩, ⟨x, y⟩\} \to ⟨x, x⟩ \in ⟨u, t⟩$
33		opex	$⊢ ⟨x, y⟩ \in V$
34	33	prid2	$⊢ ⟨x, y⟩ \in \{⟨x, x⟩, ⟨x, y⟩\}$
35		eleq2	$⊢ ⟨u, t⟩ = \{⟨x, x⟩, ⟨x, y⟩\} \to (⟨x, y⟩ \in ⟨u, t⟩ \leftrightarrow ⟨x, y⟩ \in \{⟨x, x⟩, ⟨x, y⟩\})$
36	34 35	mpbiri	$⊢ ⟨u, t⟩ = \{⟨x, x⟩, ⟨x, y⟩\} \to ⟨x, y⟩ \in ⟨u, t⟩$
37	32 36	jca	$⊢ ⟨u, t⟩ = \{⟨x, x⟩, ⟨x, y⟩\} \to (⟨x, x⟩ \in ⟨u, t⟩ \land ⟨x, y⟩ \in ⟨u, t⟩)$
38		opeq12	$⊢ (z = x \land w = x) \to ⟨z, w⟩ = ⟨x, x⟩$
39	38	3adant3	$⊢ (z = x \land w = x \land v = y) \to ⟨z, w⟩ = ⟨x, x⟩$
40	39	eleq1d	$⊢ (z = x \land w = x \land v = y) \to (⟨z, w⟩ \in ⟨u, t⟩ \leftrightarrow ⟨x, x⟩ \in ⟨u, t⟩)$
41		opeq12	$⊢ (z = x \land v = y) \to ⟨z, v⟩ = ⟨x, y⟩$
42	41	3adant2	$⊢ (z = x \land w = x \land v = y) \to ⟨z, v⟩ = ⟨x, y⟩$
43	42	eleq1d	$⊢ (z = x \land w = x \land v = y) \to (⟨z, v⟩ \in ⟨u, t⟩ \leftrightarrow ⟨x, y⟩ \in ⟨u, t⟩)$
44	40 43	anbi12d	$⊢ (z = x \land w = x \land v = y) \to ((⟨z, w⟩ \in ⟨u, t⟩ \land ⟨z, v⟩ \in ⟨u, t⟩) \leftrightarrow (⟨x, x⟩ \in ⟨u, t⟩ \land ⟨x, y⟩ \in ⟨u, t⟩))$
45		eqeq12	$⊢ (w = x \land v = y) \to (w = v \leftrightarrow x = y)$
46	45	3adant1	$⊢ (z = x \land w = x \land v = y) \to (w = v \leftrightarrow x = y)$
47	44 46	imbi12d	$⊢ (z = x \land w = x \land v = y) \to (((⟨z, w⟩ \in ⟨u, t⟩ \land ⟨z, v⟩ \in ⟨u, t⟩) \to w = v) \leftrightarrow ((⟨x, x⟩ \in ⟨u, t⟩ \land ⟨x, y⟩ \in ⟨u, t⟩) \to x = y))$
48	47	spc3gv	$⊢ (x \in V \land x \in V \land y \in V) \to (\forall z \forall w \forall v ((⟨z, w⟩ \in ⟨u, t⟩ \land ⟨z, v⟩ \in ⟨u, t⟩) \to w = v) \to ((⟨x, x⟩ \in ⟨u, t⟩ \land ⟨x, y⟩ \in ⟨u, t⟩) \to x = y))$
49	15 15 18 48	mp3an	$⊢ \forall z \forall w \forall v ((⟨z, w⟩ \in ⟨u, t⟩ \land ⟨z, v⟩ \in ⟨u, t⟩) \to w = v) \to ((⟨x, x⟩ \in ⟨u, t⟩ \land ⟨x, y⟩ \in ⟨u, t⟩) \to x = y)$
50	28 37 49	syl2im	$⊢ Fun ⟨u, t⟩ \to (⟨u, t⟩ = \{⟨x, x⟩, ⟨x, y⟩\} \to x = y)$
51	26 50	syl5bi	$⊢ Fun ⟨u, t⟩ \to ((u = \{x\} \land t = \{x, y\}) \to x = y)$
52		dfsn2	$⊢ \{x\} = \{x, x\}$
53		preq2	$⊢ x = y \to \{x, x\} = \{x, y\}$
54	52 53	syl5req	$⊢ x = y \to \{x, y\} = \{x\}$
55	54	eqeq2d	$⊢ x = y \to (t = \{x, y\} \leftrightarrow t = \{x\})$
56		eqtr3	$⊢ (u = \{x\} \land t = \{x\}) \to u = t$
57	56	expcom	$⊢ t = \{x\} \to (u = \{x\} \to u = t)$
58	55 57	syl6bi	$⊢ x = y \to (t = \{x, y\} \to (u = \{x\} \to u = t))$
59	58	com13	$⊢ u = \{x\} \to (t = \{x, y\} \to (x = y \to u = t))$
60	59	imp	$⊢ (u = \{x\} \land t = \{x, y\}) \to (x = y \to u = t)$
61	51 60	sylcom	$⊢ Fun ⟨u, t⟩ \to ((u = \{x\} \land t = \{x, y\}) \to u = t)$
62	61	exlimdvv	$⊢ Fun ⟨u, t⟩ \to (\exists x \exists y (u = \{x\} \land t = \{x, y\}) \to u = t)$
63	13 62	mpd	$⊢ Fun ⟨u, t⟩ \to u = t$
64	4 8 63	vtocl2g	$⊢ (A \in V \land B \in W) \to (Fun ⟨A, B⟩ \to A = B)$
65	64	3impia	$⊢ (A \in V \land B \in W \land Fun ⟨A, B⟩) \to A = B$

Metamath Proof Explorer

Theorem funopg

Proof