Theorem funopg 3652

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 2552	. . . . . 6 |- (u = A -> <.u, t>. = <.A, t>.)
2		funeq 3640	. . . . . 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 1524	. . . . 5 |- (u = A -> (u = t <-> A = t))
5	3, 4	imbi12d 629	. . . 4 |- (u = A -> ((Fun <.u, t>. -> u = t) <-> (Fun <.A, t>. -> A = t)))
6		opeq2 2553	. . . . . 6 |- (t = B -> <.A, t>. = <.A, B>.)
7		funeq 3640	. . . . . 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 1527	. . . . 5 |- (t = B -> (A = t <-> A = B))
10	8, 9	imbi12d 629	. . . 4 |- (t = B -> ((Fun <.A, t>. -> A = t) <-> (Fun <.A, B>. -> A = B)))
11		funrel 3638	. . . . . 6 |- (Fun <.u, t>. -> Rel <.u, t>.)
12		visset 1859	. . . . . . 7 |- u e. V
13		visset 1859	. . . . . . 7 |- t e. V
14	12, 13	relop 3365	. . . . . 6 |- (Rel <.u, t>. <-> E.xE.y(u = {x} /\ t = {x, y}))
15	11, 14	sylib 196	. . . . 5 |- (Fun <.u, t>. -> E.xE.y(u = {x} /\ t = {x, y}))
16		dffun4 3633	. . . . . . . . . 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 324	. . . . . . . . 9 |- (Fun <.u, t>. -> A.zA.wA.v((<.z, w>. e. <.u, t>. /\ <.z, v>. e. <.u, t>.) -> w = v))
18		visset 1859	. . . . . . . . . . 11 |- x e. V
19		visset 1859	. . . . . . . . . . 11 |- y e. V
20		opeq12 2554	. . . . . . . . . . . . . . . 16 |- ((z = x /\ w = x) -> <.z, w>. = <.x, x>.)
21	20	3adant3 805	. . . . . . . . . . . . . . 15 |- ((z = x /\ w = x /\ v = y) -> <.z, w>. = <.x, x>.)
22	21	eleq1d 1583	. . . . . . . . . . . . . 14 |- ((z = x /\ w = x /\ v = y) -> (<.z, w>. e. <.u, t>. <-> <.x, x>. e. <.u, t>.))
23		opeq12 2554	. . . . . . . . . . . . . . . 16 |- ((z = x /\ v = y) -> <.z, v>. = <.x, y>.)
24	23	3adant2 804	. . . . . . . . . . . . . . 15 |- ((z = x /\ w = x /\ v = y) -> <.z, v>. = <.x, y>.)
25	24	eleq1d 1583	. . . . . . . . . . . . . 14 |- ((z = x /\ w = x /\ v = y) -> (<.z, v>. e. <.u, t>. <-> <.x, y>. e. <.u, t>.))
26	22, 25	anbi12d 631	. . . . . . . . . . . . 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 1530	. . . . . . . . . . . . . 14 |- ((w = x /\ v = y) -> (w = v <-> x = y))
28	27	3adant1 803	. . . . . . . . . . . . 13 |- ((z = x /\ w = x /\ v = y) -> (w = v <-> x = y))
29	26, 28	imbi12d 629	. . . . . . . . . . . 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 1913	. . . . . . . . . . 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 922	. . . . . . . . . 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 2858	. . . . . . . . . . . . 13 |- <.x, x>. e. V
33	32	prid1 2513	. . . . . . . . . . . 12 |- <.x, x>. e. {<.x, x>., <.x, y>.}
34		eleq2 1578	. . . . . . . . . . . 12 |- (<.u, t>. = {<.x, x>., <.x, y>.} -> (<.x, x>. e. <.u, t>. <-> <.x, x>. e. {<.x, x>., <.x, y>.}))
35	33, 34	mpbiri 192	. . . . . . . . . . 11 |- (<.u, t>. = {<.x, x>., <.x, y>.} -> <.x, x>. e. <.u, t>.)
36		opex 2858	. . . . . . . . . . . . 13 |- <.x, y>. e. V
37	36	prid2 2514	. . . . . . . . . . . 12 |- <.x, y>. e. {<.x, x>., <.x, y>.}
38		eleq2 1578	. . . . . . . . . . . 12 |- (<.u, t>. = {<.x, x>., <.x, y>.} -> (<.x, y>. e. <.u, t>. <-> <.x, y>. e. {<.x, x>., <.x, y>.}))
39	37, 38	mpbiri 192	. . . . . . . . . . 11 |- (<.u, t>. = {<.x, x>., <.x, y>.} -> <.x, y>. e. <.u, t>.)
40	35, 39	jca 286	. . . . . . . . . 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 2856	. . . . . . . . . 10 |- {x, y} e. V
44	12, 13, 43	opth 2863	. . . . . . . . 9 |- (<.u, t>. = <.{x}, {x, y}>. <-> (u = {x} /\ t = {x, y}))
45		dfsn2 2478	. . . . . . . . . . . . . 14 |- {x} = {x, x}
46		preq2 2510	. . . . . . . . . . . . . 14 |- ({x} = {x, x} -> {{x}, {x}} = {{x}, {x, x}})
47	45, 46	ax-mp 7	. . . . . . . . . . . . 13 |- {{x}, {x}} = {{x}, {x, x}}
48		dfsn2 2478	. . . . . . . . . . . . 13 |- {{x}} = {{x}, {x}}
49		df-op 2474	. . . . . . . . . . . . 13 |- <.x, x>. = {{x}, {x, x}}
50	47, 48, 49	3eqtr4ri 1549	. . . . . . . . . . . 12 |- <.x, x>. = {{x}}
51		preq1 2509	. . . . . . . . . . . 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 2474	. . . . . . . . . . . 12 |- <.x, y>. = {{x}, {x, y}}
54		preq2 2510	. . . . . . . . . . . 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 2474	. . . . . . . . . . 11 |- <.{x}, {x, y}>. = {{{x}}, {{x}, {x, y}}}
57	52, 55, 56	3eqtr4ri 1549	. . . . . . . . . 10 |- <.{x}, {x, y}>. = {<.x, x>., <.x, y>.}
58	57	eqeq2i 1528	. . . . . . . . 9 |- (<.u, t>. = <.{x}, {x, y}>. <-> <.u, t>. = {<.x, x>., <.x, y>.})
59	44, 58	bitr3i 173	. . . . . . . 8 |- ((u = {x} /\ t = {x, y}) <-> <.u, t>. = {<.x, x>., <.x, y>.})
60	42, 59	syl5ib 204	. . . . . . 7 |- (Fun <.u, t>. -> ((u = {x} /\ t = {x, y}) -> x = y))
61		preq2 2510	. . . . . . . . . . . 12 |- (x = y -> {x, x} = {x, y})
62	61, 45	syl5req 1563	. . . . . . . . . . 11 |- (x = y -> {x, y} = {x})
63	62	eqeq2d 1529	. . . . . . . . . 10 |- (x = y -> (t = {x, y} <-> t = {x}))
64		eqtr3 1537	. . . . . . . . . . 11 |- ((u = {x} /\ t = {x}) -> u = t)
65	64	expcom 372	. . . . . . . . . 10 |- (t = {x} -> (u = {x} -> u = t))
66	63, 65	syl6bi 212	. . . . . . . . 9 |- (x = y -> (t = {x, y} -> (u = {x} -> u = t)))
67	66	com13 33	. . . . . . . 8 |- (u = {x} -> (t = {x, y} -> (x = y -> u = t)))
68	67	imp 348	. . . . . . 7 |- ((u = {x} /\ t = {x, y}) -> (x = y -> u = t))
69	60, 68	sylcom 51	. . . . . 6 |- (Fun <.u, t>. -> ((u = {x} /\ t = {x, y}) -> u = t))
70	69	19.23advv 1335	. . . . 5 |- (Fun <.u, t>. -> (E.xE.y(u = {x} /\ t = {x, y}) -> u = t))
71	15, 70	mpd 26	. . . 4 |- (Fun <.u, t>. -> u = t)
72	5, 10, 71	vtocl2g 1896	. . 3 |- ((A e. V /\ B e. C) -> (Fun <.A, B>. -> A = B))
73		opprc1b 2872	. . . . . 6 |- (-. A e. V <-> (/) e. <.A, B>.)
74		funrel 3638	. . . . . . . 8 |- (Fun <.A, B>. -> Rel <.A, B>.)
75		df-rel 3266	. . . . . . . . 9 |- (Rel <.A, B>. <-> <.A, B>. (_ (V X. V))
76		0nelxp 3326	. . . . . . . . . 10 |- -. (/) e. (V X. V)
77		ssel 2115	. . . . . . . . . 10 |- (<.A, B>. (_ (V X. V) -> ((/) e. <.A, B>. -> (/) e. (V X. V)))
78	76, 77	mtoi 106	. . . . . . . . 9 |- (<.A, B>. (_ (V X. V) -> -. (/) e. <.A, B>.)
79	75, 78	sylbi 197	. . . . . . . 8 |- (Rel <.A, B>. -> -. (/) e. <.A, B>.)
80	74, 79	syl 10	. . . . . . 7 |- (Fun <.A, B>. -> -. (/) e. <.A, B>.)
81	80	con2i 97	. . . . . 6 |- ((/) e. <.A, B>. -> -. Fun <.A, B>.)
82	73, 81	sylbi 197	. . . . 5 |- (-. A e. V -> -. Fun <.A, B>.)
83	82	pm2.21d 78	. . . 4 |- (-. A e. V -> (Fun <.A, B>. -> A = B))
84	83	adantr 389	. . 3 |- ((-. A e. V /\ B e. C) -> (Fun <.A, B>. -> A = B))
85	72, 84	pm2.61ian 479	. 2 |- (B e. C -> (Fun <.A, B>. -> A = B))
86	85	imp 348	1 |- ((B e. C /\ Fun <.A, B>.) -> A = B)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   /\ wa 221   /\ w3a 781  A.wal 990   = wceq 992   e. wcel 994  E.wex 1016  Vcvv 1857   (_ wss 2099  (/)c0 2332  {csn 2467  {cpr 2468  <.cop 2469   X. cxp 3249  Rel wrel 3256  Fun wfun 3257

This theorem is referenced by:  nvex 8477

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-br 2693  df-opab 2741  df-id 2913  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-fun 3273

Copyright terms: Public domain