Theorem relop 3275

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 3185	. 2 |- (Rel <.A, B>. <-> <.A, B>. (_ (V X. V))
2		dfss2 2058	. . . . 5 |- (<.A, B>. (_ (V X. V) <-> A.z(z e. <.A, B>. -> z e. (V X. V)))
3		visset 1813	. . . . . . . . 9 |- z e. V
4	3	elop 2783	. . . . . . . 8 |- (z e. <.A, B>. <-> (z = {A} \/ z = {A, B}))
5		elvv 3228	. . . . . . . 8 |- (z e. (V X. V) <-> E.xE.y z = <.x, y>.)
6	4, 5	imbi12i 188	. . . . . . 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	bitr 173	. . . . . 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 999	. . . . 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 1067	. . . . 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	3bitr 177	. . . 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		eqtr2t 1493	. . . . . . . . . . . . . 14 |- ((A = {x, y} /\ A = {w}) -> {x, y} = {w})
14		visset 1813	. . . . . . . . . . . . . . . 16 |- x e. V
15		visset 1813	. . . . . . . . . . . . . . . 16 |- y e. V
16		visset 1813	. . . . . . . . . . . . . . . 16 |- w e. V
17	14, 15, 16	preqsn 2486	. . . . . . . . . . . . . . 15 |- ({x, y} = {w} <-> (x = y /\ y = w))
18	17	pm3.26bi 322	. . . . . . . . . . . . . 14 |- ({x, y} = {w} -> x = y)
19	13, 18	syl 10	. . . . . . . . . . . . 13 |- ((A = {x, y} /\ A = {w}) -> x = y)
20		preq2 2449	. . . . . . . . . . . . . . . . . . . 20 |- (x = y -> {x, x} = {x, y})
21		dfsn2 2420	. . . . . . . . . . . . . . . . . . . 20 |- {x} = {x, x}
22	20, 21	syl5req 1520	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> {x, y} = {x})
23	22	eqeq2d 1486	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (A = {x, y} <-> A = {x}))
24	20, 21	syl5eq 1519	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> {x} = {x, y})
25	24	eqeq2d 1486	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (B = {x} <-> B = {x, y}))
26	23, 25	anbi12d 628	. . . . . . . . . . . . . . . . 17 |- (x = y -> ((A = {x, y} /\ B = {x}) <-> (A = {x} /\ B = {x, y})))
27	26	biimpd 153	. . . . . . . . . . . . . . . 16 |- (x = y -> ((A = {x, y} /\ B = {x}) -> (A = {x} /\ B = {x, y})))
28	27	exp3a 375	. . . . . . . . . . . . . . 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 374	. . . . . . . . . . 11 |- (A = {w} -> (A = {x, y} -> (B = {x} -> (A = {x} /\ B = {x, y}))))
33	32	imp3a 361	. . . . . . . . . 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 1477	. . . . . . . . . 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 2803	. . . . . . . . . 10 |- (<.x, y>. = {A, B} <-> ((A = {x} /\ B = {x, y}) \/ (A = {x, y} /\ B = {x})))
39	35, 38	bitr 173	. . . . . . . . 9 |- ({A, B} = <.x, y>. <-> ((A = {x} /\ B = {x, y}) \/ (A = {x, y} /\ B = {x})))
40	34, 39	syl5ib 206	. . . . . . . 8 |- (A = {w} -> ({A, B} = <.x, y>. -> (A = {x} /\ B = {x, y})))
41	40	19.22dvv 1292	. . . . . . 7 |- (A = {w} -> (E.xE.y{A, B} = <.x, y>. -> E.xE.y(A = {x} /\ B = {x, y})))
42	41	19.23aiv 1295	. . . . . 6 |- (E.w A = {w} -> (E.xE.y{A, B} = <.x, y>. -> E.xE.y(A = {x} /\ B = {x, y})))
43	42	imp 350	. . . . 5 |- ((E.w A = {w} /\ E.xE.y{A, B} = <.x, y>.) -> E.xE.y(A = {x} /\ B = {x, y}))
44		snex 2750	. . . . . . 7 |- {A} e. V
45		eqeq1 1481	. . . . . . . 8 |- (z = {A} -> (z = {A} <-> {A} = {A}))
46		eqeq1 1481	. . . . . . . . . 10 |- (z = {A} -> (z = <.x, y>. <-> {A} = <.x, y>.))
47		eqcom 1477	. . . . . . . . . . 11 |- ({A} = <.x, y>. <-> <.x, y>. = {A})
48	14, 15, 36	opeqsn 2802	. . . . . . . . . . 11 |- (<.x, y>. = {A} <-> (x = y /\ A = {x}))
49	47, 48	bitr 173	. . . . . . . . . 10 |- ({A} = <.x, y>. <-> (x = y /\ A = {x}))
50	46, 49	syl6bb 536	. . . . . . . . 9 |- (z = {A} -> (z = <.x, y>. <-> (x = y /\ A = {x})))
51	50	2exbidv 1281	. . . . . . . 8 |- (z = {A} -> (E.xE.y z = <.x, y>. <-> E.xE.y(x = y /\ A = {x})))
52	45, 51	imbi12d 626	. . . . . . 7 |- (z = {A} -> ((z = {A} -> E.xE.y z = <.x, y>.) <-> ({A} = {A} -> E.xE.y(x = y /\ A = {x}))))
53	44, 52	cla4v 1868	. . . . . 6 |- (A.z(z = {A} -> E.xE.y z = <.x, y>.) -> ({A} = {A} -> E.xE.y(x = y /\ A = {x})))
54		sneq 2417	. . . . . . . . 9 |- (w = x -> {w} = {x})
55	54	eqeq2d 1486	. . . . . . . 8 |- (w = x -> (A = {w} <-> A = {x}))
56	55	cbvexv 1315	. . . . . . 7 |- (E.w A = {w} <-> E.x A = {x})
57		19.41v 1305	. . . . . . . . 9 |- (E.y(x = y /\ A = {x}) <-> (E.y x = y /\ A = {x}))
58		a9e 1125	. . . . . . . . . 10 |- E.y y = x
59		equcom 1129	. . . . . . . . . . 11 |- (y = x <-> x = y)
60	59	exbii 1051	. . . . . . . . . 10 |- (E.y y = x <-> E.y x = y)
61	58, 60	mpbi 189	. . . . . . . . 9 |- E.y x = y
62	57, 61	mpbiran 728	. . . . . . . 8 |- (E.y(x = y /\ A = {x}) <-> A = {x})
63	62	exbii 1051	. . . . . . 7 |- (E.xE.y(x