Theorem relop 4429

Description: A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)

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

Dummy variables w v z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rel 4295	. 2 |- ( Rel <.A , B >. <-> <.A , B >. C_ ( _V X. _V))
2		dfss2 2928	. . . . 5 |- ( <.A , B >. C_ ( _V X. _V) <-> A.z(z e. <.A , B >. -> z e. ( _V X. _V)))
3		vex 2554	. . . . . . . . . 10 |- z e. _V
4		relop.1	. . . . . . . . . 10 |- A e. _V
5		relop.2	. . . . . . . . . 10 |- B e. _V
6	3, 4, 5	elop 3959	. . . . . . . . 9 |- (z e. <.A , B >. <-> (z = {A } \/ z = {A , B }))
7		elvv 4345	. . . . . . . . 9 |- (z e. ( _V X. _V) <-> E.xE.y z = <.x , y >.)
8	6, 7	imbi12i 228	. . . . . . . 8 |- ((z e. <.A , B >. -> z e. ( _V X. _V)) <-> ((z = {A } \/ z = {A , B }) -> E.xE.y z = <.x , y >.))
9		jaob 630	. . . . . . . 8 |- (((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 >.)))
10	8, 9	bitri 173	. . . . . . 7 |- ((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 >.)))
11	10	albii 1356	. . . . . 6 |- (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 >.)))
12		19.26 1367	. . . . . 6 |- (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 >.)))
13	11, 12	bitri 173	. . . . 5 |- (A.z(z e. <.A , B >. -> z e. ( _V X. _V)) <-> (A.z(z = {A } -> E.xE.y z = <.x , y >.) /\ A.z(z = {A , B } -> E.xE.y z = <.x , y >.)))
14	2, 13	bitri 173	. . . 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 >.)))
15		snexgOLD 3926	. . . . . . . 8 |- (A e. _V -> {A } e. _V)
16	4, 15	ax-mp 7	. . . . . . 7 |- {A } e. _V
17		eqeq1 2043	. . . . . . . 8 |- (z = {A } -> (z = {A } <-> {A } = {A }))
18		eqeq1 2043	. . . . . . . . . 10 |- (z = {A } -> (z = <.x , y >. <-> {A } = <.x , y >.))
19		eqcom 2039	. . . . . . . . . . 11 |- ( {A } = <.x , y >. <-> <.x , y >. = {A })
20		vex 2554	. . . . . . . . . . . 12 |- x e. _V
21		vex 2554	. . . . . . . . . . . 12 |- y e. _V
22	20, 21, 4	opeqsn 3980	. . . . . . . . . . 11 |- ( <.x , y >. = {A } <-> (x = y /\ A = {x }))
23	19, 22	bitri 173	. . . . . . . . . 10 |- ( {A } = <.x , y >. <-> (x = y /\ A = {x }))
24	18, 23	syl6bb 185	. . . . . . . . 9 |- (z = {A } -> (z = <.x , y >. <-> (x = y /\ A = {x })))
25	24	2exbidv 1745	. . . . . . . 8 |- (z = {A } -> (E.xE.y z = <.x , y >. <-> E.xE.y(x = y /\ A = {x })))
26	17, 25	imbi12d 223	. . . . . . 7 |- (z = {A } -> ((z = {A } -> E.xE.y z = <.x , y >.) <-> ( {A } = {A } -> E.xE.y(x = y /\ A = {x }))))
27	16, 26	spcv 2640	. . . . . 6 |- (A.z(z = {A } -> E.xE.y z = <.x , y >.) -> ( {A } = {A } -> E.xE.y(x = y /\ A = {x })))
28		sneq 3378	. . . . . . . . 9 |- (w = x -> {w } = {x })
29	28	eqeq2d 2048	. . . . . . . 8 |- (w = x -> (A = {w } <-> A = {x }))
30	29	cbvexv 1792	. . . . . . 7 |- (E.w A = {w } <-> E.x A = {x })
31		a9ev 1584	. . . . . . . . . 10 |- E.y y = x
32		equcom 1590	. . . . . . . . . . 11 |- (y = x <-> x = y)
33	32	exbii 1493	. . . . . . . . . 10 |- (E.y y = x <-> E.y x = y)
34	31, 33	mpbi 133	. . . . . . . . 9 |- E.y x = y
35		19.41v 1779	. . . . . . . . 9 |- (E.y(x = y /\ A = {x }) <-> (E.y x = y /\ A = {x }))
36	34, 35	mpbiran 846	. . . . . . . 8 |- (E.y(x = y /\ A = {x }) <-> A = {x })
37	36	exbii 1493	. . . . . . 7 |- (E.xE.y(x = y /\ A = {x }) <-> E.x A = {x })
38		eqid 2037	. . . . . . . 8 |- {A } = {A }
39	38	a1bi 232	. . . . . . 7 |- (E.xE.y(x = y /\ A = {x }) <-> ( {A } = {A } -> E.xE.y(x = y /\ A = {x })))
40	30, 37, 39	3bitr2ri 198	. . . . . 6 |- (( {A } = {A } -> E.xE.y(x = y /\ A = {x })) <-> E.w A = {w })
41	27, 40	sylib 127	. . . . 5 |- (A.z(z = {A } -> E.xE.y z = <.x , y >.) -> E.w A = {w })
42		eqid 2037	. . . . . 6 |- {A , B } = {A , B }
43		prexgOLD 3937	. . . . . . . 8 |- ((A e. _V /\ B e. _V) -> {A , B } e. _V)
44	4, 5, 43	mp2an 402	. . . . . . 7 |- {A , B } e. _V
45		eqeq1 2043	. . . . . . . 8 |- (z = {A , B } -> (z = {A , B } <-> {A , B } = {A , B }))
46		eqeq1 2043	. . . . . . . . 9 |- (z = {A , B } -> (z = <.x , y >. <-> {A , B } = <.x , y >.))
47	46	2exbidv 1745	. . . . . . . 8 |- (z = {A , B } -> (E.xE.y z = <.x , y >. <-> E.xE.y {A , B } = <.x , y >.))
48	45, 47	imbi12d 223	. . . . . . 7 |- (z = {A , B } -> ((z = {A , B } -> E.xE.y z = <.x , y >.) <-> ( {A , B } = {A , B } -> E.xE.y {A , B } = <.x , y >.)))
49	44, 48	spcv 2640	. . . . . 6 |- (A.z(z = {A , B } -> E.xE.y z = <.x , y >.) -> ( {A , B } = {A , B } -> E.xE.y {A , B } = <.x , y >.))
50	42, 49	mpi 15	. . . . 5 |- (A.z(z = {A , B } -> E.xE.y z = <.x , y >.) -> E.xE.y {A , B } = <.x , y >.)
51		eqcom 2039	. . . . . . . . . 10 |- ( {A , B } = <.x , y >. <-> <.x , y >. = {A , B })
52	20, 21, 4, 5	opeqpr 3981	. . . . . . . . . 10 |- ( <.x , y >. = {A , B } <-> ((A = {x } /\ B = {x , y }) \/ (A = {x , y } /\ B = {x })))
53	51, 52	bitri 173	. . . . . . . . 9 |- ( {A , B } = <.x , y >. <-> ((A = {x } /\ B = {x , y }) \/ (A = {x , y } /\ B = {x })))
54		idd 21	. . . . . . . . . 10 |- (A = {w } -> ((A = {x } /\ B = {x , y }) -> (A = {x } /\ B = {x , y })))
55		eqtr2 2055	. . . . . . . . . . . . . 14 |- ((A = {x , y } /\ A = {w }) -> {x , y } = {w })
56		vex 2554	. . . . . . . . . . . . . . . 16 |- w e. _V
57	20, 21, 56	preqsn 3537	. . . . . . . . . . . . . . 15 |- ( {x , y } = {w } <-> (x = y /\ y = w))
58	57	simplbi 259	. . . . . . . . . . . . . 14 |- ( {x , y } = {w } -> x = y)
59	55, 58	syl 14	. . . . . . . . . . . . 13 |- ((A = {x , y } /\ A = {w }) -> x = y)
60		dfsn2 3381	. . . . . . . . . . . . . . . . . . . 20 |- {x } = {x , x }
61		preq2 3439	. . . . . . . . . . . . . . . . . . . 20 |- (x = y -> {x , x } = {x , y })
62	60, 61	syl5req 2082	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> {x , y } = {x })
63	62	eqeq2d 2048	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (A = {x , y } <-> A = {x }))
64	60, 61	syl5eq 2081	. . . . . . . . . . . . . . . . . . 19 |- (x = y -> {x } = {x , y })
65	64	eqeq2d 2048	. . . . . . . . . . . . . . . . . 18 |- (x = y -> (B = {x } <-> B = {x , y }))
66	63, 65	anbi12d 442	. . . . . . . . . . . . . . . . 17 |- (x = y -> ((A = {x , y } /\ B = {x }) <-> (A = {x } /\ B = {x , y })))
67	66	biimpd 132	. . . . . . . . . . . . . . . 16 |- (x = y -> ((A = {x , y } /\ B = {x }) -> (A = {x } /\ B = {x , y })))
68	67	expd 245	. . . . . . . . . . . . . . 15 |- (x = y -> (A = {x , y } -> (B = {x } -> (A = {x } /\ B = {x , y }))))
69	68	com12 27	. . . . . . . . . . . . . 14 |- (A = {x , y } -> (x = y -> (B = {x } -> (A = {x } /\ B = {x , y }))))
70	69	adantr 261	. . . . . . . . . . . . 13 |- ((A = {x , y } /\ A = {w }) -> (x = y -> (B = {x } -> (A = {x } /\ B = {x , y }))))
71	59, 70	mpd 13	. . . . . . . . . . . 12 |- ((A = {x , y } /\ A = {w }) -> (B = {x } -> (A = {x } /\ B = {x , y })))
72	71	expcom 109	. . . . . . . . . . 11 |- (A = {w } -> (A = {x , y } -> (B = {x } -> (A = {x } /\ B = {x , y }))))
73	72	impd 242	. . . . . . . . . 10 |- (A = {w } -> ((A = {x , y } /\ B = {x }) -> (A = {x } /\ B = {x , y })))
74	54, 73	jaod 636	. . . . . . . . 9 |- (A = {w } -> (((A = {x } /\ B = {x , y }) \/ (A = {x , y } /\ B = {x })) -> (A = {x } /\ B = {x , y })))
75	53, 74	syl5bi 141	. . . . . . . 8 |- (A = {w } -> ( {A , B } = <.x , y >. -> (A = {x } /\ B = {x , y })))
76	75	2eximdv 1759	. . . . . . 7 |- (A = {w } -> (E.xE.y {A , B } = <.x , y >. -> E.xE.y(A = {x } /\ B = {x , y })))
77	76	exlimiv 1486	. . . . . 6 |- (E.w A = {w } -> (E.xE.y {A , B } = <.x , y >. -> E.xE.y(A = {x } /\ B = {x , y })))
78	77	imp 115	. . . . 5 |- ((E.w A = {w } /\ E.xE.y {A , B } = <.x , y >.) -> E.xE.y(A = {x } /\ B = {x , y }))
79	41, 50, 78	syl2an 273	. . . 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 }))
80	14, 79	sylbi 114	. . 3 |- ( <.A , B >. C_ ( _V X. _V) -> E.xE.y(A = {x } /\ B = {x , y }))
81		simpr 103	. . . . . . . . . . 11 |- ((A = {x } /\ z = {A }) -> z = {A })
82		equid 1586	. . . . . . . . . . . . . 14 |- x = x
83	82	jctl 297	. . . . . . . . . . . . 13 |- (A = {x } -> (x = x /\ A = {x }))
84	20, 20, 4	opeqsn 3980	. . . . . . . . . . . . 13 |- ( <.x , x >. = {A } <-> (x = x /\ A = {x }))
85	83, 84	sylibr 137	. . . . . . . . . . . 12 |- (A = {x } -> <.x , x >. = {A })
86	85	adantr 261	. . . . . . . . . . 11 |- ((A = {x } /\ z = {A }) -> <.x , x >. = {A })
87	81, 86	eqtr4d 2072	. . . . . . . . . 10 |- ((A = {x } /\ z = {A }) -> z = <.x , x >.)
88		opeq12 3542	. . . . . . . . . . . 12 |- ((w = x /\ v = x) -> <.w , v >. = <.x , x >.)
89	88	eqeq2d 2048	. . . . . . . . . . 11 |- ((w = x /\ v = x) -> (z = <.w , v >. <-> z = <.x , x >.))
90	20, 20, 89	spc2ev 2642	. . . . . . . . . 10 |- (z = <.x , x >. -> E.wE.v z = <.w , v >.)
91	87, 90	syl 14	. . . . . . . . 9 |- ((A = {x } /\ z = {A }) -> E.wE.v z = <.w , v >.)
92	91	adantlr 446	. . . . . . . 8 |- (((A = {x } /\ B = {x , y }) /\ z = {A }) -> E.wE.v z = <.w , v >.)
93		preq12 3440	. . . . . . . . . . . 12 |- ((A = {x } /\ B = {x , y }) -> {A , B } = { {x } , {x , y } })
94	93	eqeq2d 2048	. . . . . . . . . . 11 |- ((A = {x } /\ B = {x , y }) -> (z = {A , B } <-> z = { {x } , {x , y } }))
95	94	biimpa 280	. . . . . . . . . 10 |- (((A = {x } /\ B = {x , y }) /\ z = {A , B }) -> z = { {x } , {x , y } })
96	20, 21	dfop 3539	. . . . . . . . . 10 |- <.x , y >. = { {x } , {x , y } }
97	95, 96	syl6eqr 2087	. . . . . . . . 9 |- (((A = {x } /\ B = {x , y }) /\ z = {A , B }) -> z = <.x , y >.)
98		opeq12 3542	. . . . . . . . . . 11 |- ((w = x /\ v = y) -> <.w , v >. = <.x , y >.)
99	98	eqeq2d 2048	. . . . . . . . . 10 |- ((w = x /\ v = y) -> (z = <.w , v >. <-> z = <.x , y >.))
100	20, 21, 99	spc2ev 2642	. . . . . . . . 9 |- (z = <.x , y >. -> E.wE.v z = <.w , v >.)
101	97, 100	syl 14	. . . . . . . 8 |- (((A = {x } /\ B = {x , y }) /\ z = {A , B }) -> E.wE.v z = <.w , v >.)
102	92, 101	jaodan 709	. . . . . . 7 |- (((A = {x } /\ B = {x , y }) /\ (z = {A } \/ z = {A , B })) -> E.wE.v z = <.w , v >.)
103	102	ex 108	. . . . . 6 |- ((A = {x } /\ B = {x , y }) -> ((z = {A } \/ z = {A , B }) -> E.wE.v z = <.w , v >.))
104		elvv 4345	. . . . . 6 |- (z e. ( _V X. _V) <-> E.wE.v z = <.w , v >.)
105	103, 6, 104	3imtr4g 194	. . . . 5 |- ((A = {x } /\ B = {x , y }) -> (z e. <.A , B >. -> z e. ( _V X. _V)))
106	105	ssrdv 2945	. . . 4 |- ((A = {x } /\ B = {x , y }) -> <.A , B >. C_ ( _V X. _V))
107	106	exlimivv 1773	. . 3 |- (E.xE.y(A = {x } /\ B = {x , y }) -> <.A , B >. C_ ( _V X. _V))
108	80, 107	impbii 117	. 2 |- ( <.A , B >. C_ ( _V X. _V) <-> E.xE.y(A = {x } /\ B = {x , y }))
109	1, 108	bitri 173	1 |- ( Rel <.A , B >. <-> E.xE.y(A = {x } /\ B = {x , y }))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 628  A.wal 1240   = wceq 1242  E.wex 1378   e. wcel 1390   _Vcvv 2551   C_ wss 2911   {csn 3367   {cpr 3368   <.cop 3370   X. cxp 4286   Rel wrel 4293

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-xp 4294  df-rel 4295

This theorem is referenced by:  funopg  4877