Theorem relop 4486

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 4352	. 2 |- ( Rel <. A , B >. <-> <. A , B >. C_ ( _V X. _V ) )
2		dfss2 2934	. . . . 5 |- ( <. A , B >. C_ ( _V X. _V ) <-> A. z ( z e. <. A , B >. -> z e. ( _V X. _V ) ) )
3		vex 2560	. . . . . . . . . 10 |- z e. _V
4		relop.1	. . . . . . . . . 10 |- A e. _V
5		relop.2	. . . . . . . . . 10 |- B e. _V
6	3, 4, 5	elop 3968	. . . . . . . . 9 |- ( z e. <. A , B >. <-> ( z = { A } \/ z = { A , B } ) )
7		elvv 4402	. . . . . . . . 9 |- ( z e. ( _V X. _V ) <-> E. x E. 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. x E. y z = <. x , y >. ) )
9		jaob 631	. . . . . . . 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 173	. . . . . . 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 1359	. . . . . 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 1370	. . . . . 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 173	. . . . 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 173	. . . 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		snexgOLD 3935	. . . . . . . 8 |- ( A e. _V -> { A } e. _V )
16	4, 15	ax-mp 7	. . . . . . 7 |- { A } e. _V
17		eqeq1 2046	. . . . . . . 8 |- ( z = { A } -> ( z = { A } <-> { A } = { A } ) )
18		eqeq1 2046	. . . . . . . . . 10 |- ( z = { A } -> ( z = <. x , y >. <-> { A } = <. x , y >. ) )
19		eqcom 2042	. . . . . . . . . . 11 |- ( { A } = <. x , y >. <-> <. x , y >. = { A } )
20		vex 2560	. . . . . . . . . . . 12 |- x e. _V
21		vex 2560	. . . . . . . . . . . 12 |- y e. _V
22	20, 21, 4	opeqsn 3989	. . . . . . . . . . 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 1748	. . . . . . . 8 |- ( z = { A } -> ( E. x E. y z = <. x , y >. <-> E. x E. y ( x = y /\ A = { x } ) ) )
26	17, 25	imbi12d 223	. . . . . . 7 |- ( z = { A } -> ( ( z = { A } -> E. x E. y z = <. x , y >. ) <-> ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) ) )
27	16, 26	spcv 2646	. . . . . 6 |- ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) -> ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) )
28		sneq 3386	. . . . . . . . 9 |- ( w = x -> { w } = { x } )
29	28	eqeq2d 2051	. . . . . . . 8 |- ( w = x -> ( A = { w } <-> A = { x } ) )
30	29	cbvexv 1795	. . . . . . 7 |- ( E. w A = { w } <-> E. x A = { x } )
31		a9ev 1587	. . . . . . . . . 10 |- E. y y = x
32		equcom 1593	. . . . . . . . . . 11 |- ( y = x <-> x = y )
33	32	exbii 1496	. . . . . . . . . 10 |- ( E. y y = x <-> E. y x = y )
34	31, 33	mpbi 133	. . . . . . . . 9 |- E. y x = y
35		19.41v 1782	. . . . . . . . 9 |- ( E. y ( x = y /\ A = { x } ) <-> ( E. y x = y /\ A = { x } ) )
36	34, 35	mpbiran 847	. . . . . . . 8 |- ( E. y ( x = y /\ A = { x } ) <-> A = { x } )
37	36	exbii 1496	. . . . . . 7 |- ( E. x E. y ( x = y /\ A = { x } ) <-> E. x A = { x } )
38		eqid 2040	. . . . . . . 8 |- { A } = { A }
39	38	a1bi 232	. . . . . . 7 |- ( E. x E. y ( x = y /\ A = { x } ) <-> ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) )
40	30, 37, 39	3bitr2ri 198	. . . . . 6 |- ( ( { A } = { A } -> E. x E. y ( x = y /\ A = { x } ) ) <-> E. w A = { w } )
41	27, 40	sylib 127	. . . . 5 |- ( A. z ( z = { A } -> E. x E. y z = <. x , y >. ) -> E. w A = { w } )
42		eqid 2040	. . . . . 6 |- { A , B } = { A , B }
43		prexgOLD 3946	. . . . . . . 8 |- ( ( A e. _V /\ B e. _V ) -> { A , B } e. _V )
44	4, 5, 43	mp2an 402	. . . . . . 7 |- { A , B } e. _V
45		eqeq1 2046	. . . . . . . 8 |- ( z = { A , B } -> ( z = { A , B } <-> { A , B } = { A , B } ) )
46		eqeq1 2046	. . . . . . . . 9 |- ( z = { A , B } -> ( z = <. x , y >. <-> { A , B } = <. x , y >. ) )
47	46	2exbidv 1748	. . . . . . . 8 |- ( z = { A , B } -> ( E. x E. y z = <. x , y >. <-> E. x E. y { A , B } = <. x , y >. ) )
48	45, 47	imbi12d 223	. . . . . . 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 >. ) ) )
49	44, 48	spcv 2646	. . . . . 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 >. ) )
50	42, 49	mpi 15	. . . . 5 |- ( A. z ( z = { A , B } -> E. x E. y z = <. x , y >. ) -> E. x E. y { A , B } = <. x , y >. )
51		eqcom 2042	. . . . . . . . . 10 |- ( { A , B } = <. x , y >. <-> <. x , y >. = { A , B } )
52	20, 21, 4, 5	opeqpr 3990	. . . . . . . . . 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 2058	. . . . . . . . . . . . . 14 |- ( ( A = { x , y } /\ A = { w } ) -> { x , y } = { w } )
56		vex 2560	. . . . . . . . . . . . . . . 16 |- w e. _V
57	20, 21, 56	preqsn 3546	. . . . . . . . . . . . . . 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 3389	. . . . . . . . . . . . . . . . . . . 20 |- { x } = { x , x }
61		preq2 3448	. . . . . . . . . . . . . . . . . . . 20 |- ( x = y -> { x , x } = { x , y } )
62	60, 61	syl5req 2085	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> { x , y } = { x } )
63	62	eqeq2d 2051	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( A = { x , y } <-> A = { x } ) )
64	60, 61	syl5eq 2084	. . . . . . . . . . . . . . . . . . 19 |- ( x = y -> { x } = { x , y } )
65	64	eqeq2d 2051	. . . . . . . . . . . . . . . . . 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 637	. . . . . . . . 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 1762	. . . . . . 7 |- ( A = { w } -> ( E. x E. y { A , B } = <. x , y >. -> E. x E. y ( A = { x } /\ B = { x , y } ) ) )
77	76	exlimiv 1489	. . . . . 6 |- ( E. w A = { w } -> ( E. x E. y { A , B } = <. x , y >. -> E. x E. y ( A = { x } /\ B = { x , y } ) ) )
78	77	imp 115	. . . . 5 |- ( ( E. w A = { w } /\ E. x E. y { A , B } = <. x , y >. ) -> E. x E. y ( A = { x } /\ B = { x , y } ) )
79	41, 50, 78	syl2an 273	. . . 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 } ) )
80	14, 79	sylbi 114	. . 3 |- ( <. A , B >. C_ ( _V X. _V ) -> E. x E. y ( A = { x } /\ B = { x , y } ) )
81		simpr 103	. . . . . . . . . . 11 |- ( ( A = { x } /\ z = { A } ) -> z = { A } )
82		equid 1589	. . . . . . . . . . . . . 14 |- x = x
83	82	jctl 297	. . . . . . . . . . . . 13 |- ( A = { x } -> ( x = x /\ A = { x } ) )
84	20, 20, 4	opeqsn 3989	. . . . . . . . . . . . 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 2075	. . . . . . . . . 10 |- ( ( A = { x } /\ z = { A } ) -> z = <. x , x >. )
88		opeq12 3551	. . . . . . . . . . . 12 |- ( ( w = x /\ v = x ) -> <. w , v >. = <. x , x >. )
89	88	eqeq2d 2051	. . . . . . . . . . 11 |- ( ( w = x /\ v = x ) -> ( z = <. w , v >. <-> z = <. x , x >. ) )
90	20, 20, 89	spc2ev 2648	. . . . . . . . . 10 |- ( z = <. x , x >. -> E. w E. v z = <. w , v >. )
91	87, 90	syl 14	. . . . . . . . 9 |- ( ( A = { x } /\ z = { A } ) -> E. w E. v z = <. w , v >. )
92	91	adantlr 446	. . . . . . . 8 |- ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A } ) -> E. w E. v z = <. w , v >. )
93		preq12 3449	. . . . . . . . . . . 12 |- ( ( A = { x } /\ B = { x , y } ) -> { A , B } = { { x } , { x , y } } )
94	93	eqeq2d 2051	. . . . . . . . . . 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 3548	. . . . . . . . . 10 |- <. x , y >. = { { x } , { x , y } }
97	95, 96	syl6eqr 2090	. . . . . . . . 9 |- ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A , B } ) -> z = <. x , y >. )
98		opeq12 3551	. . . . . . . . . . 11 |- ( ( w = x /\ v = y ) -> <. w , v >. = <. x , y >. )
99	98	eqeq2d 2051	. . . . . . . . . 10 |- ( ( w = x /\ v = y ) -> ( z = <. w , v >. <-> z = <. x , y >. ) )
100	20, 21, 99	spc2ev 2648	. . . . . . . . 9 |- ( z = <. x , y >. -> E. w E. v z = <. w , v >. )
101	97, 100	syl 14	. . . . . . . 8 |- ( ( ( A = { x } /\ B = { x , y } ) /\ z = { A , B } ) -> E. w E. v z = <. w , v >. )
102	92, 101	jaodan 710	. . . . . . 7 |- ( ( ( A = { x } /\ B = { x , y } ) /\ ( z = { A } \/ z = { A , B } ) ) -> E. w E. v z = <. w , v >. )
103	102	ex 108	. . . . . 6 |- ( ( A = { x } /\ B = { x , y } ) -> ( ( z = { A } \/ z = { A , B } ) -> E. w E. v z = <. w , v >. ) )
104		elvv 4402	. . . . . 6 |- ( z e. ( _V X. _V ) <-> E. w E. 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 2951	. . . 4 |- ( ( A = { x } /\ B = { x , y } ) -> <. A , B >. C_ ( _V X. _V ) )
107	106	exlimivv 1776	. . 3 |- ( E. x E. 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. x E. y ( A = { x } /\ B = { x , y } ) )
109	1, 108	bitri 173	1 |- ( Rel <. A , B >. <-> E. x E. y ( A = { x } /\ B = { x , y } ) )

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 629   A.wal 1241   = wceq 1243   E.wex 1381   e. wcel 1393   _Vcvv 2557   C_ wss 2917   {csn 3375   {cpr 3376   <.cop 3378   X. cxp 4343   Rel wrel 4350

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 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-opab 3819  df-xp 4351  df-rel 4352

This theorem is referenced by:  funopg  4934