Theorem relop 3365

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 3266	. 2 |- (Rel <.A, B>. <-> <.A, B>. (_ (V X. V))
2		dfss2 2110	. . . . 5 |- (<.A, B>. (_ (V X. V) <-> A.z(z e. <.A, B>. -> z e. (V X. V)))
3		visset 1859	. . . . . . . . 9 |- z e. V
4	3	elop 2859	. . . . . . . 8 |- (z e. <.A, B>. <-> (z = {A} \/ z = {A, B}))
5		elvv 3313	. . . . . . . 8 |- (z e. (V X. V) <-> E.xE.y z = <.x, y>.)
6	4, 5	imbi12i 186	. . . . . . 7 |- ((z e. <.A, B>. -> z e. (V X. V)) <-> ((z = {A} \/ z = {A, B}) -> E.xE.y z = <.x, y>.))
7		jaob 422	. . . . . . 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 171	. . . . . 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 1035	. . . . 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 1103	. . . . 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 175	. . . 4 |- (<.A, B>. (_ (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 61	. . . . . . . . . 10 |- (A = {w} -> ((A = {x} /\ B = {x, y}) -> (A = {x} /\ B = {x, y})))
13		eqtr2 1536	. . . . . . . . . . . . . 14 |- ((A = {x, y} /\ A = {w}) -> {x, y} = {w})
14		visset 1859	. . . . . . . . . . . . . . . 16 |- x e. V
15		visset 1859	. . . . . . . . . . . . . . . 16 |- y e. V
16		visset 1859	. . . . . . . . . . . . . . . 16 |- w e. V
17	14, 15, 16	preqsn 2551	. . . . . . . . . . . . . . 15 |- ({x, y} = {w} <-> (x = y /\ y = w))
18	17	pm3.26bi 320	. . . . . . . . . . . . . 14 |- ({x, y} = {w} -> x = y)
19	13, 18	syl 10	. . . . . . . . . . . . 13 |- ((A = {x, y} /\ A = {w}) -> x = y)
20		preq2 2510	. . . . . . . . . . . . . . . . . . . 20 |- (x = y -> {x, x} = {x, y})
21		dfsn2 2478	. . . . . . . . . . . . . . . . . . . 20 |- {x} = {x, x}
22	20, 21	syl5req 1563	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> {x, y} = {x})
23	22	eqeq2d 1529	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (A = {x, y} <-> A = {x}))
24	20, 21	syl5eq 1562	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> {x} = {x, y})
25	24	eqeq2d 1529	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (B = {x} <-> B = {x, y}))
26	23, 25	anbi12d 631	. . . . . . . . . . . . . . . . 17 |- (x = y -> ((A = {x, y} /\ B = {x}) <-> (A = {x} /\ B = {x, y})))
27	26	biimpd 151	. . . . . . . . . . . . . . . 16 |- (x = y -> ((A = {x, y} /\ B = {x}) -> (A = {x} /\ B = {x, y})))
28	27	exp3a 374	. . . . . . . . . . . . . . 15 |- (x = y -> (A = {x, y} -> (B = {x} -> (A = {x} /\ B = {x, y}))))
29	28	com12 11	. . . . . . . . . . . . . 14 |- (A = {x, y} -> (x = y -> (B = {x} -> (A = {x} /\ B = {x, y}))))
30	29	adantr 389	. . . . . . . . . . . . 13 |- ((A = {x, y} /\ A = {w}) -> (x = y -> (B = {x} -> (A = {x} /\ B = {x, y}))))
31	19, 30	mpd 26	. . . . . . . . . . . 12 |- ((A = {x, y} /\ A = {w}) -> (B = {x} -> (A = {x} /\ B = {x, y})))
32	31	expcom 372	. . . . . . . . . . 11 |- (A = {w} -> (A = {x, y} -> (B = {x} -> (A = {x} /\ B = {x, y}))))
33	32	imp3a 359	. . . . . . . . . 10 |- (A = {w} -> ((A = {x, y} /\ B = {x}) -> (A = {x} /\ B = {x, y})))
34	12, 33	jaod 424	. . . . . . . . 9 |- (A = {w} -> (((A = {x} /\ B = {x, y}) \/ (A = {x, y} /\ B = {x})) -> (A = {x} /\ B = {x, y})))
35		eqcom 1520	. . . . . . . . . 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 2880	. . . . . . . . . 10 |- (<.x, y>. = {A, B} <-> ((A = {x} /\ B = {x, y}) \/ (A = {x, y} /\ B = {x})))
39	35, 38	bitri 171	. . . . . . . . 9 |- ({A, B} = <.x, y>. <-> ((A = {x} /\ B = {x, y}) \/ (A = {x, y} /\ B = {x})))
40	34, 39	syl5ib 204	. . . . . . . 8 |- (A = {w} -> ({A, B} = <.x, y>. -> (A = {x} /\ B = {x, y})))
41	40	19.22dvv 1330	. . . . . . 7 |- (A = {w} -> (E.xE.y{A, B} = <.x, y>. -> E.xE.y(A = {x} /\ B = {x, y})))
42	41	19.23aiv 1333	. . . . . 6 |- (E.w A = {w} -> (E.xE.y{A, B} = <.x, y>. -> E.xE.y(A = {x} /\ B = {x, y})))
43	42	imp 348	. . . . 5 |- ((E.w A = {w} /\ E.xE.y{A, B} = <.x, y>.) -> E.xE.y(A = {x} /\ B = {x, y}))
44		snex 2826	. . . . . . 7 |- {A} e. V
45		eqeq1 1524	. . . . . . . 8 |- (z = {A} -> (z = {A} <-> {A} = {A}))
46		eqeq1 1524	. . . . . . . . . 10 |- (z = {A} -> (z = <.x, y>. <-> {A} = <.x, y>.))
47		eqcom 1520	. . . . . . . . . . 11 |- ({A} = <.x, y>. <-> <.x, y>. = {A})
48	14, 15, 36	opeqsn 2879	. . . . . . . . . . 11 |- (<.x, y>. = {A} <-> (x = y /\ A = {x}))
49	47, 48	bitri 171	. . . . . . . . . 10 |- ({A} = <.x, y>. <-> (x = y /\ A = {x}))
50	46, 49	syl6bb 539	. . . . . . . . 9 |- (z = {A} -> (z = <.x, y>. <-> (x = y /\ A = {x})))
51	50	2exbidv 1319	. . . . . . . 8 |- (z = {A} -> (E.xE.y z = <.x, y>. <-> E.xE.y(x = y /\ A = {x})))
52	45, 51	imbi12d 629	. . . . . . 7 |- (z = {A} -> ((z = {A} -> E.xE.y z = <.x, y>.) <-> ({A} = {A} -> E.xE.y(x = y /\ A = {x}))))
53	44, 52	cla4v 1914	. . . . . 6 |- (A.z(z = {A} -> E.xE.y z = <.x, y>.) -> ({A} = {A} -> E.xE.y(x = y /\ A = {x})))
54		sneq 2475	. . . . . . . . 9 |- (w = x -> {w} = {x})
55	54	eqeq2d 1529	. . . . . . . 8 |- (w = x -> (A = {w} <-> A = {x}))
56	55	cbvexv 1353	. . . . . . 7 |- (E.w A = {w} <-> E.x A = {x})
57		19.41v 1343	. . . . . . . . 9 |- (E.y(x = y /\ A = {x}) <-> (E.y x = y /\ A = {x}))
58		a9e 1161	. . . . . . . . . 10 |- E.y y = x
59		equcom 1166	. . . . . . . . . . 11 |- (y = x <-> x = y)
60	59	exbii 1087	. . . . . . . . . 10 |- (E.y y = x <-> E.y x = y)
61	58, 60	mpbi 187	. . . . . . . . 9 |- E.y x = y
62	57, 61	mpbiran 733	. . . . . . . 8 |- (E.y(x = y /\ A = {x}) <-> A = {x})
63	62	exbii 1087	. . . . . . 7 |- (E.xE.y(x = y /\ A = {x}) <-> E.x A = {x})
64		eqid 1518	. . . . . . . 8 |- {A} = {A}
65	64	a1bi 195	. . . . . . 7 |- (E.xE.y(x = y /\ A = {x}) <-> ({A} = {A} -> E.xE.y(x = y /\ A = {x})))
66	56, 63, 65	3bitr2ri 178	. . . . . 6 |- (({A} = {A} -> E.xE.y(x = y /\ A = {x})) <-> E.w A = {w})
67	53, 66	sylib 196	. . . . 5 |- (A.z(z = {A} -> E.xE.y z = <.x, y>.) -> E.w A = {w})
68		eqid 1518	. . . . . 6 |- {A, B} = {A, B}
69		prex 2857	. . . . . . 7 |- {A, B} e. V
70		eqeq1 1524	. . . . . . . 8 |- (z = {A, B} -> (z = {A, B} <-> {A, B} = {A, B}))
71		eqeq1 1524	. . . . . . . . 9 |- (z = {A, B} -> (z = <.x, y>. <-> {A, B} = <.x, y>.))
72	71	2exbidv 1319	. . . . . . . 8 |- (z = {A, B} -> (E.xE.y z = <.x, y>. <-> E.xE.y{A, B} = <.x, y>.))
73	70, 72	imbi12d 629	. . . . . . 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 1914	. . . . . 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 44	. . . . 5 |- (A.z(z = {A, B} -> E.xE.y z = <.x, y>.) -> E.xE.y{A, B} = <.x, y>.)
76	43, 67, 75	syl2an 456	. . . 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 197	. . 3 |- (<.A, B>. (_ (V X. V) -> E.xE.y(A = {x} /\ B = {x, y}))
78		pm3.27 321	. . . . . . . . . . 11 |- ((A = {x} /\ z = {A}) -> z = {A})
79		equid 1162	. . . . . . . . . . . . . 14 |- x = x
80	79	jctl 288	. . . . . . . . . . . . 13 |- (A = {x} -> (x = x /\ A = {x}))
81	14, 14, 36	opeqsn 2879	. . . . . . . . . . . . 13 |- (<.x, x>. = {A} <-> (x = x /\ A = {x}))
82	80, 81	sylibr 198	. . . . . . . . . . . 12 |- (A = {x} -> <.x, x>. = {A})
83	82	adantr 389	. . . . . . . . . . 11 |- ((A = {x} /\ z = {A}) -> <.x, x>. = {A})
84	78, 83	eqtr4d 1553	. . . . . . . . . 10 |- ((A = {x} /\ z = {A}) -> z = <.x, x>.)
85		opeq12 2554	. . . . . . . . . . . 12 |- ((w = x /\ v = x) -> <.w, v>. = <.x, x>.)
86	85	eqeq2d 1529	. . . . . . . . . . 11 |- ((w = x /\ v = x) -> (z = <.w, v>. <-> z = <.x, x>.))
87	14, 14, 86	cla42ev 1916	. . . . . . . . . 10 |- (z = <.x, x>. -> E.wE.v z = <.w, v>.)
88	84, 87	syl 10	. . . . . . . . 9 |- ((A = {x} /\ z = {A}) -> E.wE.v z = <.w, v>.)
89	88	adantlr 393	. . . . . . . 8 |- (((A = {x} /\ B = {x, y}) /\ z = {A}) -> E.wE.v z = <.w, v>.)
90		preq1 2509	. . . . . . . . . . . . 13 |- (A = {x} -> {A, B} = {{x}, B})
91		preq2 2510	. . . . . . . . . . . . 13 |- (B = {x, y} -> {{x}, B} = {{x}, {x, y}})
92	90, 91	sylan9eq 1570	. . . . . . . . . . . 12 |- ((A = {x} /\ B = {x, y}) -> {A, B} = {{x}, {x, y}})
93	92	eqeq2d 1529	. . . . . . . . . . 11 |- ((A = {x} /\ B = {x, y}) -> (z = {A, B} <-> z = {{x}, {x, y}}))
94	93	biimpa 416	. . . . . . . . . 10 |- (((A = {x} /\ B = {x, y}) /\ z = {A, B}) -> z = {{x}, {x, y}})
95		df-op 2474	. . . . . . . . . 10 |- <.x, y>. = {{x}, {x, y}}
96	94, 95	syl6eqr 1568	. . . . . . . . 9 |- (((A = {x} /\ B = {x, y}) /\ z = {A, B}) -> z = <.x, y>.)
97		opeq12 2554	. . . . . . . . . . 11 |- ((w = x /\ v = y) -> <.w, v>. = <.x, y>.)
98	97	eqeq2d 1529	. . . . . . . . . 10 |- ((w = x /\ v = y) -> (z = <.w, v>. <-> z = <.x, y>.))
99	14, 15, 98	cla42ev 1916	. . . . . . . . 9 |- (z = <.x, y>. -> E.wE.v z = <.w, v>.)
100	96, 99	syl 10	. . . . . . . 8 |- (((A = {x} /\ B = {x, y}) /\ z = {A, B}) -> E.wE.v z = <.w, v>.)
101	89, 100	jaodan 426	. . . . . . 7 |- (((A = {x} /\ B = {x, y}) /\ (z = {A} \/ z = {A, B})) -> E.wE.v z = <.w, v>.)
102	101	ex 371	. . . . . 6 |- ((A = {x} /\ B = {x, y}) -> ((z = {A} \/ z = {A, B}) -> E.wE.v z = <.w, v>.))
103		elvv 3313	. . . . . 6 |- (z e. (V X. V) <-> E.wE.v z = <.w, v>.)
104	102, 4, 103	3imtr4g 556	. . . . 5 |- ((A = {x} /\ B = {x, y}) -> (z e. <.A, B>. -> z e. (V X. V)))
105	104	ssrdv 2122	. . . 4 |- ((A = {x} /\ B = {x, y}) -> <.A, B>. (_ (V X. V))
106	105	19.23aivv 1334	. . 3 |- (E.xE.y(A = {x} /\ B = {x, y}) -> <.A, B>. (_ (V X. V))
107	77, 106	impbii 155	. 2 |- (<.A, B>. (_ (V X. V) <-> E.xE.y(A = {x} /\ B = {x, y}))
108	1, 107	bitri 171	1 |- (Rel <.A, B>. <-> E.xE.y(A = {x} /\ B = {x, y}))

Syntax hints:   -> wi 3   <-> wb 144   \/ wo 220   /\ wa 221  A.wal 990   = wceq 992   e. wcel 994  E.wex 1016  Vcvv 1857   (_ wss 2099  {csn 2467  {cpr 2468  <.cop 2469   X. cxp 3249  Rel wrel 3256

This theorem is referenced by:  funopg 3652

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-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  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-opab 2741  df-xp 3265  df-rel 3266

Copyright terms: Public domain