Theorem relop 4113

Description: A necessary and sufficient condition for a Kuratowski ordered pair to be a relation.

Hypotheses

Ref	Expression
relop.1	|- A e. _V
relop.2	|- B e. _V

Assertion

Ref	Expression
relop	|- (Rel <.A, B>. <-> E.xE.y(A = {x} /\ B = {x, y}))

Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem relop

Step	Hyp	Ref	Expression
1		df-rel 4001	. 2 |- (Rel <.A, B>. <-> <.A, B>. C_ (_V X. _V))
2		dfss2 2610	. . . . 5 |- (<.A, B>. C_ (_V X. _V) <-> A.z(z e. <.A, B>. -> z e. (_V X. _V)))
3		visset 2295	. . . . . . . . 9 |- z e. _V
4	3	elop 3528	. . . . . . . 8 |- (z e. <.A, B>. <-> (z = {A} \/ z = {A, B}))
5		elvv 4053	. . . . . . . 8 |- (z e. (_V X. _V) <-> E.xE.y z = <.x, y>.)
6	4, 5	imbi12i 205	. . . . . . 7 |- ((z e. <.A, B>. -> z e. (_V X. _V)) <-> ((z = {A} \/ z = {A, B}) -> E.xE.y z = <.x, y>.))
7		jaob 467	. . . . . . 7 |- (((z = {A} \/ z = {A, B}) -> E.xE.y z = <.x, y>.) <-> ((z = {A} -> E.xE.y z = <.x, y>.) /\ (z = {A, B} -> E.xE.y z = <.x, y>.)))
8	6, 7	bitri 190	. . . . . 6 |- ((z e. <.A, B>. -> z e. (_V X. _V)) <-> ((z = {A} -> E.xE.y z = <.x, y>.) /\ (z = {A, B} -> E.xE.y z = <.x, y>.)))
9	8	albii 1346	. . . . 5 |- (A.z(z e. <.A, B>. -> z e. (_V X. _V)) <-> A.z((z = {A} -> E.xE.y z = <.x, y>.) /\ (z = {A, B} -> E.xE.y z = <.x, y>.)))
10		19.26 1416	. . . . 5 |- (A.z((z = {A} -> E.xE.y z = <.x, y>.) /\ (z = {A, B} -> E.xE.y z = <.x, y>.)) <-> (A.z(z = {A} -> E.xE.y z = <.x, y>.) /\ A.z(z = {A, B} -> E.xE.y z = <.x, y>.)))
11	2, 9, 10	3bitri 194	. . . 4 |- (<.A, B>. C_ (_V X. _V) <-> (A.z(z = {A} -> E.xE.y z = <.x, y>.) /\ A.z(z = {A, B} -> E.xE.y z = <.x, y>.)))
12		idd 75	. . . . . . . . . 10 |- (A = {w} -> ((A = {x} /\ B = {x, y}) -> (A = {x} /\ B = {x, y})))
13		eqtr2 1905	. . . . . . . . . . . . . 14 |- ((A = {x, y} /\ A = {w}) -> {x, y} = {w})
14		visset 2295	. . . . . . . . . . . . . . . 16 |- x e. _V
15		visset 2295	. . . . . . . . . . . . . . . 16 |- y e. _V
16		visset 2295	. . . . . . . . . . . . . . . 16 |- w e. _V
17	14, 15, 16	preqsn 3157	. . . . . . . . . . . . . . 15 |- ({x, y} = {w} <-> (x = y /\ y = w))
18	17	simplbi 349	. . . . . . . . . . . . . 14 |- ({x, y} = {w} -> x = y)
19	13, 18	syl 12	. . . . . . . . . . . . 13 |- ((A = {x, y} /\ A = {w}) -> x = y)
20		preq2 3099	. . . . . . . . . . . . . . . . . . . 20 |- (x = y -> {x, x} = {x, y})
21		dfsn2 3057	. . . . . . . . . . . . . . . . . . . 20 |- {x} = {x, x}
22	20, 21	syl5req 1941	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> {x, y} = {x})
23	22	eqeq2d 1895	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (A = {x, y} <-> A = {x}))
24	20, 21	syl5eq 1940	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> {x} = {x, y})
25	24	eqeq2d 1895	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (B = {x} <-> B = {x, y}))
26	23, 25	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (x = y -> ((A = {x, y} /\ B = {x}) <-> (A = {x} /\ B = {x, y})))
27	26	biimpd 170	. . . . . . . . . . . . . . . 16 |- (x = y -> ((A = {x, y} /\ B = {x}) -> (A = {x} /\ B = {x, y})))
28	27	exp3a 405	. . . . . . . . . . . . . . 15 |- (x = y -> (A = {x, y} -> (B = {x} -> (A = {x} /\ B = {x, y}))))
29	28	com12 14	. . . . . . . . . . . . . 14 |- (A = {x, y} -> (x = y -> (B = {x} -> (A = {x} /\ B = {x, y}))))
30	29	adantr 425	. . . . . . . . . . . . 13 |- ((A = {x, y} /\ A = {w}) -> (x = y -> (B = {x} -> (A = {x} /\ B = {x, y}))))
31	19, 30	mpd 29	. . . . . . . . . . . 12 |- ((A = {x, y} /\ A = {w}) -> (B = {x} -> (A = {x} /\ B = {x, y})))
32	31	expcom 403	. . . . . . . . . . 11 |- (A = {w} -> (A = {x, y} -> (B = {x} -> (A = {x} /\ B = {x, y}))))
33	32	imp3a 388	. . . . . . . . . 10 |- (A = {w} -> ((A = {x, y} /\ B = {x}) -> (A = {x} /\ B = {x, y})))
34	12, 33	jaod 469	. . . . . . . . 9 |- (A = {w} -> (((A = {x} /\ B = {x, y}) \/ (A = {x, y} /\ B = {x})) -> (A = {x} /\ B = {x, y})))
35		eqcom 1886	. . . . . . . . . 10 |- ({A, B} = <.x, y>. <-> <.x, y>. = {A, B})
36		relop.1	. . . . . . . . . . 11 |- A e. _V
37		relop.2	. . . . . . . . . . 11 |- B e. _V
38	36, 37	opeqpr 3550	. . . . . . . . . 10 |- (<.x, y>. = {A, B} <-> ((A = {x} /\ B = {x, y}) \/ (A = {x, y} /\ B = {x})))
39	35, 38	bitri 190	. . . . . . . . 9 |- ({A, B} = <.x, y>. <-> ((A = {x} /\ B = {x, y}) \/ (A = {x, y} /\ B = {x})))
40	34, 39	syl5ib 223	. . . . . . . 8 |- (A = {w} -> ({A, B} = <.x, y>. -> (A = {x} /\ B = {x, y})))
41	40	2eximdv 1671	. . . . . . 7 |- (A = {w} -> (E.xE.y{A, B} = <.x, y>. -> E.xE.y(A = {x} /\ B = {x, y})))
42	41	19.23aiv 1674	. . . . . 6 |- (E.w A = {w} -> (E.xE.y{A, B} = <.x, y>. -> E.xE.y(A = {x} /\ B = {x, y})))
43	42	imp 377	. . . . 5 |- ((E.w A = {w} /\ E.xE.y{A, B} = <.x, y>.) -> E.xE.y(A = {x} /\ B = {x, y}))
44		snex 3492	. . . . . . 7 |- {A} e. _V
45		eqeq1 1890	. . . . . . . 8 |- (z = {A} -> (z = {A} <-> {A} = {A}))
46		eqeq1 1890	. . . . . . . . . 10 |- (z = {A} -> (z = <.x, y>. <-> {A} = <.x, y>.))
47		eqcom 1886	. . . . . . . . . . 11 |- ({A} = <.x, y>. <-> <.x, y>. = {A})
48	14, 15, 36	opeqsn 3549	. . . . . . . . . . 11 |- (<.x, y>. = {A} <-> (x = y /\ A = {x}))
49	47, 48	bitri 190	. . . . . . . . . 10 |- ({A} = <.x, y>. <-> (x = y /\ A = {x}))
50	46, 49	syl6bb 595	. . . . . . . . 9 |- (z = {A} -> (z = <.x, y>. <-> (x = y /\ A = {x})))
51	50	2exbidv 1659	. . . . . . . 8 |- (z = {A} -> (E.xE.y z = <.x, y>. <-> E.xE.y(x = y /\ A = {x})))
52	45, 51	imbi12d 688	. . . . . . 7 |- (z = {A} -> ((z = {A} -> E.xE.y z = <.x, y>.) <-> ({A} = {A} -> E.xE.y(x = y /\ A = {x}))))
53	44, 52	cla4v 2370	. . . . . 6 |- (A.z(z = {A} -> E.xE.y z = <.x, y>.) -> ({A} = {A} -> E.xE.y(x = y /\ A = {x})))
54		sneq 3054	. . . . . . . . 9 |- (w = x -> {w} = {x})
55	54	eqeq2d 1895	. . . . . . . 8 |- (w = x -> (A = {w} <-> A = {x}))
56	55	cbvexv 1697	. . . . . . 7 |- (E.w A = {w} <-> E.x A = {x})
57		19.41v 1685	. . . . . . . . 9 |- (E.y(x = y /\ A = {x}) <-> (E.y x = y /\ A = {x}))
58		a9e 1483	. . . . . . . . . 10 |- E.y y = x
59		equcom 1488	. . . . . . . . . . 11 |- (y = x <-> x = y)
60	59	exbii 1398	. . . . . . . . . 10 |- (E.y y = x <-> E.y x = y)
61	58, 60	mpbi 206	. . . . . . . . 9 |- E.y x = y
62	57, 61	mpbiran 798	. . . . . . . 8 |- (E.y(x = y /\ A = {x}) <-> A = {x})
63	62	exbii 1398	. . . . . . 7 |- (E.xE.y(x = y /\ A = {x}) <-> E.x A = {x})
64		eqid 1884	. . . . . . . 8 |- {A} = {A}
65	64	a1bi 214	. . . . . . 7 |- (E.xE.y(x = y /\ A = {x}) <-> ({A} = {A} -> E.xE.y(x = y /\ A = {x})))
66	56, 63, 65	3bitr2ri 197	. . . . . 6 |- (({A} = {A} -> E.xE.y(x = y /\ A = {x})) <-> E.w A = {w})
67	53, 66	sylib 215	. . . . 5 |- (A.z(z = {A} -> E.xE.y z = <.x, y>.) -> E.w A = {w})
68		eqid 1884	. . . . . 6 |- {A, B} = {A, B}
69		prex 3526	. . . . . . 7 |- {A, B} e. _V
70		eqeq1 1890	. . . . . . . 8 |- (z = {A, B} -> (z = {A, B} <-> {A, B} = {A, B}))
71		eqeq1 1890	. . . . . . . . 9 |- (z = {A, B} -> (z = <.x, y>. <-> {A, B} = <.x, y>.))
72	71	2exbidv 1659	. . . . . . . 8 |- (z = {A, B} -> (E.xE.y z = <.x, y>. <-> E.xE.y{A, B} = <.x, y>.))
73	70, 72	imbi12d 688	. . . . . . 7 |- (z = {A, B} -> ((z = {A, B} -> E.xE.y z = <.x, y>.) <-> ({A, B} = {A, B} -> E.xE.y{A, B} = <.x, y>.)))
74	69, 73	cla4v 2370	. . . . . 6 |- (A.z(z = {A, B} -> E.xE.y z = <.x, y>.) -> ({A, B} = {A, B} -> E.xE.y{A, B} = <.x, y>.))
75	68, 74	mpi 55	. . . . 5 |- (A.z(z = {A, B} -> E.xE.y z = <.x, y>.) -> E.xE.y{A, B} = <.x, y>.)
76	43, 67, 75	syl2an 503	. . . 4 |- ((A.z(z = {A} -> E.xE.y z = <.x, y>.) /\ A.z(z = {A, B} -> E.xE.y z = <.x, y>.)) -> E.xE.y(A = {x} /\ B = {x, y}))
77	11, 76	sylbi 216	. . 3 |- (<.A, B>. C_ (_V X. _V) -> E.xE.y(A = {x} /\ B = {x, y}))
78		simpr 350	. . . . . . . . . . 11 |- ((A = {x} /\ z = {A}) -> z = {A})
79		equid 1484	. . . . . . . . . . . . . 14 |- x = x
80	79	jctl 314	. . . . . . . . . . . . 13 |- (A = {x} -> (x = x /\ A = {x}))
81	14, 14, 36	opeqsn 3549	. . . . . . . . . . . . 13 |- (<.x, x>. = {A} <-> (x = x /\ A = {x}))
82	80, 81	sylibr 217	. . . . . . . . . . . 12 |- (A = {x} -> <.x, x>. = {A})
83	82	adantr 425	. . . . . . . . . . 11 |- ((A = {x} /\ z = {A}) -> <.x, x>. = {A})
84	78, 83	eqtr4d 1928	. . . . . . . . . 10 |- ((A = {x} /\ z = {A}) -> z = <.x, x>.)
85		opeq12 3160	. . . . . . . . . . . 12 |- ((w = x /\ v = x) -> <.w, v>. = <.x, x>.)
86	85	eqeq2d 1895	. . . . . . . . . . 11 |- ((w = x /\ v = x) -> (z = <.w, v>. <-> z = <.x, x>.))
87	14, 14, 86	cla42ev 2372	. . . . . . . . . 10 |- (z = <.x, x>. -> E.wE.v z = <.w, v>.)
88	84, 87	syl 12	. . . . . . . . 9 |- ((A = {x} /\ z = {A}) -> E.wE.v z = <.w, v>.)
89	88	adantlr 429	. . . . . . . 8 |- (((A = {x} /\ B = {x, y}) /\ z = {A}) -> E.wE.v z = <.w, v>.)
90		preq1 3098	. . . . . . . . . . . . 13 |- (A = {x} -> {A, B} = {{x}, B})
91		preq2 3099	. . . . . . . . . . . . 13 |- (B = {x, y} -> {{x}, B} = {{x}, {x, y}})
92	90, 91	sylan9eq 1948	. . . . . . . . . . . 12 |- ((A = {x} /\ B = {x, y}) -> {A, B} = {{x}, {x, y}})
93	92	eqeq2d 1895	. . . . . . . . . . 11 |- ((A = {x} /\ B = {x, y}) -> (z = {A, B} <-> z = {{x}, {x, y}}))
94	93	biimpa 460	. . . . . . . . . 10 |- (((A = {x} /\ B = {x, y}) /\ z = {A, B}) -> z = {{x}, {x, y}})
95		df-op 3053	. . . . . . . . . 10 |- <.x, y>. = {{x}, {x, y}}
96	94, 95	syl6eqr 1946	. . . . . . . . 9 |- (((A = {x} /\ B = {x, y}) /\ z = {A, B}) -> z = <.x, y>.)
97		opeq12 3160	. . . . . . . . . . 11 |- ((w = x /\ v = y) -> <.w, v>. = <.x, y>.)
98	97	eqeq2d 1895	. . . . . . . . . 10 |- ((w = x /\ v = y) -> (z = <.w, v>. <-> z = <.x, y>.))
99	14, 15, 98	cla42ev 2372	. . . . . . . . 9 |- (z = <.x, y>. -> E.wE.v z = <.w, v>.)
100	96, 99	syl 12	. . . . . . . 8 |- (((A = {x} /\ B = {x, y}) /\ z = {A, B}) -> E.wE.v z = <.w, v>.)
101	89, 100	jaodan 471	. . . . . . 7 |- (((A = {x} /\ B = {x, y}) /\ (z = {A} \/ z = {A, B})) -> E.wE.v z = <.w, v>.)
102	101	ex 402	. . . . . 6 |- ((A = {x} /\ B = {x, y}) -> ((z = {A} \/ z = {A, B}) -> E.wE.v z = <.w, v>.))
103		elvv 4053	. . . . . 6 |- (z e. (_V X. _V) <-> E.wE.v z = <.w, v>.)
104	102, 4, 103	3imtr4g 612	. . . . 5 |- ((A = {x} /\ B = {x, y}) -> (z e. <.A, B>. -> z e. (_V X. _V)))
105	104	ssrdv 2622	. . . 4 |- ((A = {x} /\ B = {x, y}) -> <.A, B>. C_ (_V X. _V))
106	105	19.23aivv 1675	. . 3 |- (E.xE.y(A = {x} /\ B = {x, y}) -> <.A, B>. C_ (_V X. _V))
107	77, 106	impbii 174	. 2 |- (<.A, B>. C_ (_V X. _V) <-> E.xE.y(A = {x} /\ B = {x, y}))
108	1, 107	bitri 190	1 |- (Rel <.A, B>. <-> E.xE.y(A = {x} /\ B = {x, y}))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292   C_ wss 2593  {csn 3044  {cpr 3045  <.cop 3046   X. cxp 3984  Rel wrel 3991

This theorem is referenced by:  funopg 4454

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-opab 3396  df-xp 4000  df-rel 4001

Copyright terms: Public domain