Theorem funopg 3553

Description: A Kuratowski ordered pair is a function only if its components are equal.

Assertion

Ref	Expression
funopg	|- ((B e. C /\ Fun <.A, B>.) -> A = B)

Proof of Theorem funopg

Step	Hyp	Ref	Expression
1		opeq1 2491	. . . . . 6 |- (u = A -> <.u, t>. = <.A, t>.)
2		funeq 3541	. . . . . 6 |- (<.u, t>. = <.A, t>. -> (Fun <.u, t>. <-> Fun <.A, t>.))
3	1, 2	syl 10	. . . . 5 |- (u = A -> (Fun <.u, t>. <-> Fun <.A, t>.))
4		eqeq1 1484	. . . . 5 |- (u = A -> (u = t <-> A = t))
5	3, 4	imbi12d 628	. . . 4 |- (u = A -> ((Fun <.u, t>. -> u = t) <-> (Fun <.A, t>. -> A = t)))
6		opeq2 2492	. . . . . 6 |- (t = B -> <.A, t>. = <.A, B>.)
7		funeq 3541	. . . . . 6 |- (<.A, t>. = <.A, B>. -> (Fun <.A, t>. <-> Fun <.A, B>.))
8	6, 7	syl 10	. . . . 5 |- (t = B -> (Fun <.A, t>. <-> Fun <.A, B>.))
9		eqeq2 1487	. . . . 5 |- (t = B -> (A = t <-> A = B))
10	8, 9	imbi12d 628	. . . 4 |- (t = B -> ((Fun <.A, t>. -> A = t) <-> (Fun <.A, B>. -> A = B)))
11		funrel 3539	. . . . . 6 |- (Fun <.u, t>. -> Rel <.u, t>.)
12		visset 1816	. . . . . . 7 |- u e. V
13		visset 1816	. . . . . . 7 |- t e. V
14	12, 13	relop 3281	. . . . . 6 |- (Rel <.u, t>. <-> E.xE.y(u = {x} /\ t = {x, y}))
15	11, 14	sylib 198	. . . . 5 |- (Fun <.u, t>. -> E.xE.y(u = {x} /\ t = {x, y}))
16		dffun4 3534	. . . . . . . . . 10 |- (Fun <.u, t>. <-> (Rel <.u, t>. /\ A.zA.wA.v((<.z, w>. e. <.u, t>. /\ <.z, v>. e. <.u, t>.) -> w = v)))
17	16	pm3.27bi 326	. . . . . . . . 9 |- (Fun <.u, t>. -> A.zA.wA.v((<.z, w>. e. <.u, t>. /\ <.z, v>. e. <.u, t>.) -> w = v))
18		visset 1816	. . . . . . . . . . 11 |- x e. V
19		visset 1816	. . . . . . . . . . 11 |- y e. V
20		opeq12 2493	. . . . . . . . . . . . . . . 16 |- ((z = x /\ w = x) -> <.z, w>. = <.x, x>.)
21	20	3adant3 801	. . . . . . . . . . . . . . 15 |- ((z = x /\ w = x /\ v = y) -> <.z, w>. = <.x, x>.)
22	21	eleq1d 1543	. . . . . . . . . . . . . 14 |- ((z = x /\ w = x /\ v = y) -> (<.z, w>. e. <.u, t>. <-> <.x, x>. e. <.u, t>.))
23		opeq12 2493	. . . . . . . . . . . . . . . 16 |- ((z = x /\ v = y) -> <.z, v>. = <.x, y>.)
24	23	3adant2 800	. . . . . . . . . . . . . . 15 |- ((z = x /\ w = x /\ v = y) -> <.z, v>. = <.x, y>.)
25	24	eleq1d 1543	. . . . . . . . . . . . . 14 |- ((z = x /\ w = x /\ v = y) -> (<.z, v>. e. <.u, t>. <-> <.x, y>. e. <.u, t>.))
26	22, 25	anbi12d 630	. . . . . . . . . . . . 13 |- ((z = x /\ w = x /\ v = y) -> ((<.z, w>. e. <.u, t>. /\ <.z, v>. e. <.u, t>.) <-> (<.x, x>. e. <.u, t>. /\ <.x, y>. e. <.u, t>.)))
27		eqeq12 1490	. . . . . . . . . . . . . 14 |- ((w = x /\ v = y) -> (w = v <-> x = y))
28	27	3adant1 799	. . . . . . . . . . . . 13 |- ((z = x /\ w = x /\ v = y) -> (w = v <-> x = y))
29	26, 28	imbi12d 628	. . . . . . . . . . . 12 |- ((z = x /\ w = x /\ v = y) -> (((<.z, w>. e. <.u, t>. /\ <.z, v>. e. <.u, t>.) -> w = v) <-> ((<.x, x>. e. <.u, t>. /\ <.x, y>. e. <.u, t>.) -> x = y)))
30	29	cla43gv 1870	. . . . . . . . . . 11 |- ((x e. V /\ x e. V /\ y e. V) -> (A.zA.wA.v((<.z, w>. e. <.u, t>. /\ <.z, v>. e. <.u, t>.) -> w = v) -> ((<.x, x>. e. <.u, t>. /\ <.x, y>. e. <.u, t>.) -> x = y)))
31	18, 18, 19, 30	mp3an 918	. . . . . . . . . 10 |- (A.zA.wA.v((<.z, w>. e. <.u, t>. /\ <.z, v>. e. <.u, t>.) -> w = v) -> ((<.x, x>. e. <.u, t>. /\ <.x, y>. e. <.u, t>.) -> x = y))
32		opex 2788	. . . . . . . . . . . . 13 |- <.x, x>. e. V
33	32	pri1 2454	. . . . . . . . . . . 12 |- <.x, x>. e. {<.x, x>., <.x, y>.}
34		eleq2 1538	. . . . . . . . . . . 12 |- (<.u, t>. = {<.x, x>., <.x, y>.} -> (<.x, x>. e. <.u, t>. <-> <.x, x>. e. {<.x, x>., <.x, y>.}))
35	33, 34	mpbiri 194	. . . . . . . . . . 11 |- (<.u, t>. = {<.x, x>., <.x, y>.} -> <.x, x>. e. <.u, t>.)
36		opex 2788	. . . . . . . . . . . . 13 |- <.x, y>. e. V
37	36	pri2 2455	. . . . . . . . . . . 12 |- <.x, y>. e. {<.x, x>., <.x, y>.}
38		eleq2 1538	. . . . . . . . . . . 12 |- (<.u, t>. = {<.x, x>., <.x, y>.} -> (<.x, y>. e. <.u, t>. <-> <.x, y>. e. {<.x, x>., <.x, y>.}))
39	37, 38	mpbiri 194	. . . . . . . . . . 11 |- (<.u, t>. = {<.x, x>., <.x, y>.} -> <.x, y>. e. <.u, t>.)
40	35, 39	jca 288	. . . . . . . . . 10 |- (<.u, t>. = {<.x, x>., <.x, y>.} -> (<.x, x>. e. <.u, t>. /\ <.x, y>. e. <.u, t>.))
41	31, 40	syl5 21	. . . . . . . . 9 |- (A.zA.wA.v((<.z, w>. e. <.u, t>. /\ <.z, v>. e. <.u, t>.) -> w = v) -> (<.u, t>. = {<.x, x>., <.x, y>.} -> x = y))
42	17, 41	syl 10	. . . . . . . 8 |- (Fun <.u, t>. -> (<.u, t>. = {<.x, x>., <.x, y>.} -> x = y))
43		zfpair2 2786	. . . . . . . . . 10 |- {x, y} e. V
44	12, 13, 43	opth 2793	. . . . . . . . 9 |- (<.u, t>. = <.{x}, {x, y}>. <-> (u = {x} /\ t = {x, y}))
45		dfsn2 2424	. . . . . . . . . . . . . 14 |- {x} = {x, x}
46		preq2 2453	. . . . . . . . . . . . . 14 |- ({x} = {x, x} -> {{x}, {x}} = {{x}, {x, x}})
47	45, 46	ax-mp 7	. . . . . . . . . . . . 13 |- {{x}, {x}} = {{x}, {x, x}}
48		dfsn2 2424	. . . . . . . . . . . . 13 |- {{x}} = {{x}, {x}}
49		df-op 2420	. . . . . . . . . . . . 13 |- <.x, x>. = {{x}, {x, x}}
50	47, 48, 49	3eqtr4r 1509	. . . . . . . . . . . 12 |- <.x, x>. = {{x}}
51		preq1 2452	. . . . . . . . . . . 12 |- (<.x, x>. = {{x}} -> {<.x, x>., {{x}, {x, y}}} = {{{x}}, {{x}, {x, y}}})
52	50, 51	ax-mp 7	. . . . . . . . . . 11 |- {<.x, x>., {{x}, {x, y}}} = {{{x}}, {{x}, {x, y}}}
53		df-op 2420	. . . . . . . . . . . 12 |- <.x, y>. = {{x}, {x, y}}
54		preq2 2453	. . . . . . . . . . . 12 |- (<.x, y>. = {{x}, {x, y}} -> {<.x, x>., <.x, y>.} = {<.x, x>., {{x}, {x, y}}})
55	53, 54	ax-mp 7	. . . . . . . . . . 11 |- {<.x, x>., <.x, y>.} = {<.x, x>., {{x}, {x, y}}}
56		df-op 2420	. . . . . . . . . . 11 |- <.{x}, {x, y}>. = {{{x}}, {{x}, {x, y}}}
57	52, 55, 56	3eqtr4r 1509	. . . . . . . . . 10 |- <.{x}, {x, y}>. = {<.x, x>., <.x, y>.}
58	57	eqeq2i 1488	. . . . . . . . 9 |- (<.u, t>. = <.{x}, {x, y}>. <-> <.u, t>. = {<.x, x>., <.x, y>.})
59	44, 58	bitr3 175	. . . . . . . 8 |- ((u = {x} /\ t = {x, y}) <-> <.u, t>. = {<.x, x>., <.x, y>.})
60	42, 59	syl5ib 206	. . . . . . 7 |- (Fun <.u, t>. -> ((u = {x} /\ t = {x, y}) -> x = y))
61		preq2 2453	. . . . . . . . . . . 12 |- (x = y -> {x, x} = {x, y})
62	61, 45	syl5req 1523	. . . . . . . . . . 11 |- (x = y -> {x, y} = {x})
63	62	eqeq2d 1489	. . . . . . . . . 10 |- (x =