Theorem relop 4684

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. x E. 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 4541	. 2 |- ( Rel <. A , B >. <-> <. A , B >. C_ ( _V X. _V ) )
2		dfss2 3081	. . . . 5 |- ( <. A , B >. C_ ( _V X. _V ) <-> A. z ( z e. <. A , B >. -> z e. ( _V X. _V ) ) )
3		vex 2684	. . . . . . . . . 10 |- z e. _V
4		relop.1	. . . . . . . . . 10 |- A e. _V
5		relop.2	. . . . . . . . . 10 |- B e. _V
6	3, 4, 5	elop 4148	. . . . . . . . 9 |- ( z e. <. A , B >. <-> ( z = { A } \/ z = { A , B } ) )
7		elvv 4596	. . . . . . . . 9 |- ( z e. ( _V X. _V ) <-> E. x E. y z = <. x , y >. )
8	6, 7	imbi12i 238	. . . . . . . 8 |- ( ( z e. <. A , B >. -> z e. ( _V X. _V ) ) <-> ( ( z = { A } \/ z = { A , B } ) -> E. x E. y z = <. x , y >. ) )
9		jaob 699	. . . . . . . 8 |- ( ( ( z = { A } \/ z = { A , B } ) -> E. x E. y z = <. x , y >. ) <-> ( ( z = { A } -> E. x E. y z = <. x , y >. ) /\ ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
10	8, 9	bitri 183	. . . . . . 7 |- ( ( z e. <. A , B >. -> z e. ( _V X. _V ) ) <-> ( ( z = { A } -> E. x E. y z = <. x , y >. ) /\ ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
11	10	albii 1446	. . . . . 6 |- ( A. z ( z e. <. A , B >. -> z e. ( _V X. _V ) ) <-> A. z ( ( z = { A } -> E. x E. y z = <. x , y >. ) /\ ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
12		19.26 1457	. . . . . 6 |- ( A. z ( ( z = { A } -> E. x E. y z = <. x , y >. ) /\ ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) <-> ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) /\ A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
13	11, 12	bitri 183	. . . . 5 |- ( A. z ( z e. <. A , B >. -> z e. ( _V X. _V ) ) <-> ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) /\ A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
14	2, 13	bitri 183	. . . 4 |- ( <. A , B >. C_ ( _V X. _V ) <-> ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) /\ A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) )
15	4	snex 4104	. . . . . . 7 |- { A } e. _V
16		eqeq1 2144	. . . . . . . 8 |- ( z = { A } -> ( z = { A } <-> { A } = { A } ) )
17		eqeq1 2144	. . . . . . . . . 10 |- ( z = { A } -> ( z = <. x , y >. <-> { A } = <. x , y >. ) )
18		eqcom 2139	. . . . . . . . . . 11 |- ( { A } = <. x , y >. <-> <. x , y >. = { A } )
19		vex 2684	. . . . . . . . . . . 12 |- x e. _V
20		vex 2684	. . . . . . . . . . . 12 |- y e. _V
21	19, 20, 4	opeqsn 4169	. . . . . . . . . . 11 |- ( <. x , y >. = { A } <-> ( x = y /\ A = { x } ) )
22	18, 21	bitri 183	. . . . . . . . . 10 |- ( { A } = <. x , y >. <-> ( x = y /\ A = { x } ) )
23	17, 22	syl6bb 195	. . . . . . . . 9 |- ( z = { A } -> ( z = <. x , y >. <-> ( x = y /\ A = { x } ) ) )
24	23	2exbidv 1840	. . . . . . . 8 |- ( z = { A } -> ( E. x E. y z = <. x , y >. <-> E. x E. y ( x = y /\ A = { x } ) ) )
25	16, 24	imbi12d 233	. . . . . . 7 |- ( z = { A } -> ( ( z = { A } -> E. x E. y z = <. x , y >. ) <-> ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) ) )
26	15, 25	spcv 2774	. . . . . 6 |- ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) -> ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) )
27		sneq 3533	. . . . . . . . 9 |- ( w = x -> { w } = { x } )
28	27	eqeq2d 2149	. . . . . . . 8 |- ( w = x -> ( A = { w } <-> A = { x } ) )
29	28	cbvexv 1890	. . . . . . 7 |- ( E. w A = { w } <-> E. x A = { x } )
30		a9ev 1675	. . . . . . . . . 10 |- E. y y = x
31		equcom 1682	. . . . . . . . . . 11 |- ( y = x <-> x = y )
32	31	exbii 1584	. . . . . . . . . 10 |- ( E. y y = x <-> E. y x = y )
33	30, 32	mpbi 144	. . . . . . . . 9 |- E. y x = y
34		19.41v 1874	. . . . . . . . 9 |- ( E. y ( x = y /\ A = { x } ) <-> ( E. y x = y /\ A = { x } ) )
35	33, 34	mpbiran 924	. . . . . . . 8 |- ( E. y ( x = y /\ A = { x } ) <-> A = { x } )
36	35	exbii 1584	. . . . . . 7 |- ( E. x E. y ( x = y /\ A = { x } ) <-> E. x A = { x } )
37		eqid 2137	. . . . . . . 8 |- { A } = { A }
38	37	a1bi 242	. . . . . . 7 |- ( E. x E. y ( x = y /\ A = { x } ) <-> ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) )
39	29, 36, 38	3bitr2ri 208	. . . . . 6 |- ( ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) <-> E. w A = { w } )
40	26, 39	sylib 121	. . . . 5 |- ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) -> E. w A = { w } )
41		eqid 2137	. . . . . 6 |- { A , B } = { A , B }
42		prexg 4128	. . . . . . . 8 |- ( ( A e. _V /\ B e. _V ) -> { A , B } e. _V )
43	4, 5, 42	mp2an 422	. . . . . . 7 |- { A , B } e. _V
44		eqeq1 2144	. . . . . . . 8 |- ( z = { A , B } -> ( z = { A , B } <-> { A , B } = { A , B } ) )
45		eqeq1 2144	. . . . . . . . 9 |- ( z = { A , B } -> ( z = <. x , y >. <-> { A , B } = <. x , y >. ) )
46	45	2exbidv 1840	. . . . . . . 8 |- ( z = { A , B } -> ( E. x E. y z = <. x , y >. <-> E. x E. y { A , B } = <. x , y >. ) )
47	44, 46	imbi12d 233	. . . . . . 7 |- ( z = { A , B } -> ( ( z = { A , B } -> E. x E. y z = <. x , y >. ) <-> ( { A , B } = { A , B } -> E. x E. y { A , B } = <. x , y >. ) ) )
48	43, 47	spcv 2774	. . . . . 6 |- ( A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) -> ( { A , B } = { A , B } -> E. x E. y { A , B } = <. x , y >. ) )
49	41, 48	mpi 15	. . . . 5 |- ( A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) -> E. x E. y { A , B } = <. x , y >. )
50		eqcom 2139	. . . . . . . . . 10 |- ( { A , B } = <. x , y >. <-> <. x , y >. = { A , B } )
51	19, 20, 4, 5	opeqpr 4170	. . . . . . . . . 10 |- ( <. x , y >. = { A , B } <-> ( ( A = { x } /\ B = { x , y } ) \/ ( A = { x , y } /\ B = { x } ) ) )
52	50, 51	bitri 183	. . . . . . . . 9 |- ( { A , B } = <. x , y >. <-> ( ( A = { x } /\ B = { x , y } ) \/ ( A = { x , y } /\ B = { x } ) ) )
53		idd 21	. . . . . . . . . 10 |- ( A = { w } -> ( ( A = { x } /\ B = { x , y } ) -> ( A = { x } /\ B = { x , y } ) ) )
54		eqtr2 2156	. . . . . . . . . . . . . 14 |- ( ( A = { x , y } /\ A = { w } ) -> { x , y } = { w } )
55		vex 2684	. . . . . . . . . . . . . . . 16 |- w e. _V
56	19, 20, 55	preqsn 3697	. . . . . . . . . . . . . . 15 |- ( { x , y } = { w } <-> ( x = y /\ y = w ) )
57	56	simplbi 272	. . . . . . . . . . . . . 14 |- ( { x , y } = { w } -> x = y )
58	54, 57	syl 14	. . . . . . . . . . . . 13 |- ( ( A = { x , y } /\ A = { w } ) -> x = y )
59		dfsn2 3536	. . . . . . . . . . . . . . . . . . . 20 |- { x } = { x , x }
60		preq2 3596	. . . . . . . . . . . . . . . . . . . 20 |- ( x = y -> { x , x } = { x , y } )
61	59, 60	syl5req 2183	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> { x , y } = { x } )
62	61	eqeq2d 2149	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( A = { x , y } <-> A = { x } ) )
63	59, 60	syl5eq 2182	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> { x } = { x , y } )
64	63	eqeq2d 2149	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( B = { x } <-> B = { x , y } ) )
65	62, 64	anbi12d 464	. . . . . . . . . . . . . . . . 17 |- ( x = y -> ( ( A = { x , y } /\ B = { x } ) <-> ( A = { x } /\ B = { x , y } ) ) )
66	65	biimpd 143	. . . . . . . . . . . . . . . 16 |- ( x = y -> ( ( A = { x , y } /\ B = { x } ) -> ( A = { x } /\ B = { x , y } ) ) )
67	66	expd 256	. . . . . . . . . . . . . . 15 |- ( x = y -> ( A = { x , y } -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) ) )
68	67	com12 30	. . . . . . . . . . . . . 14 |- ( A = { x , y } -> ( x = y -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) ) )
69	68	adantr 274	. . . . . . . . . . . . 13 |- ( ( A = { x , y } /\ A = { w } ) -> ( x = y -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) ) )
70	58, 69	mpd 13	. . . . . . . . . . . 12 |- ( ( A = { x , y } /\ A = { w } ) -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) )
71	70	expcom 115	. . . . . . . . . . 11 |- ( A = { w } -> ( A = { x , y } -> ( B = { x } -> ( A = { x } /\ B = { x , y } ) ) ) )
72	71	impd 252	. . . . . . . . . 10 |- ( A = { w } -> ( ( A = { x , y } /\ B = { x } ) -> ( A = { x } /\ B = { x , y } ) ) )
73	53, 72	jaod 706	. . . . . . . . 9 |- ( A = { w } -> ( ( ( A = { x } /\ B = { x , y } ) \/ ( A = { x , y } /\ B = { x } ) ) -> ( A = { x } /\ B = { x , y } ) ) )
74	52, 73	syl5bi 151	. . . . . . . 8 |- ( A = { w } -> ( { A , B } = <. x , y >. -> ( A = { x } /\ B = { x , y } ) ) )
75	74	2eximdv 1854	. . . . . . 7 |- ( A = { w } -> ( E. x E. y { A , B } = <. x , y >. -> E. x E. y ( A = { x } /\ B = { x , y } ) ) )
76	75	exlimiv 1577	. . . . . 6 |- ( E. w A = { w } -> ( E. x E. y { A , B } = <. x , y >. -> E. x E. y ( A = { x } /\ B = { x , y } ) ) )
77	76	imp 123	. . . . 5 |- ( ( E. w A = { w } /\ E. x E. y { A , B } = <. x , y >. ) -> E. x E. y ( A = { x } /\ B = { x , y } ) )
78	40, 49, 77	syl2an 287	. . . 4 |- ( ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) /\ A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) ) -> E. x E. y ( A = { x } /\ B = { x , y } ) )
79	14, 78	sylbi 120	. . 3 |- ( <. A , B >. C_ ( _V X. _V ) -> E. x E. y ( A = { x } /\ B = { x , y } ) )
80		simpr 109	. . . . . . . . . . 11 |- ( ( A = { x } /\ z = { A } ) -> z = { A } )
81		equid 1677	. . . . . . . . . . . . . 14 |- x = x
82	81	jctl 312	. . . . . . . . . . . . 13 |- ( A = { x } -> ( x = x /\ A = { x } ) )
83	19, 19, 4	opeqsn 4169	. . . . . . . . . . . . 13 |- ( <. x , x >. = { A } <-> ( x = x /\ A = { x } ) )
84	82, 83	sylibr 133	. . . . . . . . . . . 12 |- ( A = { x } -> <. x , x >. = { A } )
85	84	adantr 274	. . . . . . . . . . 11 |- ( ( A = { x } /\ z = { A } ) -> <. x , x >. = { A } )
86	80, 85	eqtr4d 2173	. . . . . . . . . 10 |- ( ( A = { x } /\ z = { A } ) -> z = <. x , x >. )
87		opeq12 3702	. . . . . . . . . . . 12 |- ( ( w = x /\ v = x ) -> <. w , v >. = <. x , x >. )
88	87	eqeq2d 2149	. . . . . . . . . . 11 |- ( ( w = x /\ v = x ) -> ( z = <. w , v >. <-> z = <. x , x >. ) )
89	19, 19, 88	spc2ev 2776	. . . . . . . . . 10 |- ( z = <. x , x >. -> E. w E. v z = <. w , v >. )
90	86, 89	syl 14	. . . . . . . . 9 |- ( ( A = { x } /\ z = { A } ) -> E. w E. v z = <. w , v >. )
91	90	adantlr 468	. . . . . . . 8 |- ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A } ) -> E. w E. v z = <. w , v >. )
92		preq12 3597	. . . . . . . . . . . 12 |- ( ( A = { x } /\ B = { x , y } ) -> { A , B } = { { x } , { x , y } } )
93	92	eqeq2d 2149	. . . . . . . . . . 11 |- ( ( A = { x } /\ B = { x , y } ) -> ( z = { A , B } <-> z = { { x } , { x , y } } ) )
94	93	biimpa 294	. . . . . . . . . 10 |- ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A , B } ) -> z = { { x } , { x , y } } )
95	19, 20	dfop 3699	. . . . . . . . . 10 |- <. x , y >. = { { x } , { x , y } }
96	94, 95	syl6eqr 2188	. . . . . . . . 9 |- ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A , B } ) -> z = <. x , y >. )
97		opeq12 3702	. . . . . . . . . . 11 |- ( ( w = x /\ v = y ) -> <. w , v >. = <. x , y >. )
98	97	eqeq2d 2149	. . . . . . . . . 10 |- ( ( w = x /\ v = y ) -> ( z = <. w , v >. <-> z = <. x , y >. ) )
99	19, 20, 98	spc2ev 2776	. . . . . . . . 9 |- ( z = <. x , y >. -> E. w E. v z = <. w , v >. )
100	96, 99	syl 14	. . . . . . . 8 |- ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A , B } ) -> E. w E. v z = <. w , v >. )
101	91, 100	jaodan 786	. . . . . . 7 |- ( ( ( A = { x } /\ B = { x , y } ) /\ ( z = { A } \/ z = { A , B } ) ) -> E. w E. v z = <. w , v >. )
102	101	ex 114	. . . . . 6 |- ( ( A = { x } /\ B = { x , y } ) -> ( ( z = { A } \/ z = { A , B } ) -> E. w E. v z = <. w , v >. ) )
103		elvv 4596	. . . . . 6 |- ( z e. ( _V X. _V ) <-> E. w E. v z = <. w , v >. )
104	102, 6, 103	3imtr4g 204	. . . . 5 |- ( ( A = { x } /\ B = { x , y } ) -> ( z e. <. A , B >. -> z e. ( _V X. _V ) ) )
105	104	ssrdv 3098	. . . 4 |- ( ( A = { x } /\ B = { x , y } ) -> <. A , B >. C_ ( _V X. _V ) )
106	105	exlimivv 1868	. . 3 |- ( E. x E. y ( A = { x } /\ B = { x , y } ) -> <. A , B >. C_ ( _V X. _V ) )
107	79, 106	impbii 125	. 2 |- ( <. A , B >. C_ ( _V X. _V ) <-> E. x E. y ( A = { x } /\ B = { x , y } ) )
108	1, 107	bitri 183	1 |- ( Rel <. A , B >. <-> E. x E. y ( A = { x } /\ B = { x , y } ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 697   A.wal 1329   = wceq 1331   E.wex 1468   e. wcel 1480   _Vcvv 2681   C_ wss 3066   {csn 3522   {cpr 3523   <.cop 3525   X. cxp 4532   Rel wrel 4539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-pr 4126

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-v 2683  df-un 3070  df-in 3072  df-ss 3079  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-opab 3985  df-xp 4540  df-rel 4541

This theorem is referenced by:  funopg  5152