MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  relop Structured version   Visualization version   Unicode version

Theorem relop 4990
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.
StepHypRef Expression
1 df-rel 4846 . 2  |-  ( Rel 
<. A ,  B >.  <->  <. A ,  B >.  C_  ( _V  X.  _V ) )
2 dfss2 3407 . . . . 5  |-  ( <. A ,  B >.  C_  ( _V  X.  _V ) 
<-> 
A. z ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
) )
3 relop.1 . . . . . . . . . 10  |-  A  e. 
_V
4 relop.2 . . . . . . . . . 10  |-  B  e. 
_V
53, 4elop 4667 . . . . . . . . 9  |-  ( z  e.  <. A ,  B >.  <-> 
( z  =  { A }  \/  z  =  { A ,  B } ) )
6 elvv 4898 . . . . . . . . 9  |-  ( z  e.  ( _V  X.  _V )  <->  E. x E. y 
z  =  <. x ,  y >. )
75, 6imbi12i 333 . . . . . . . 8  |-  ( ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
)  <->  ( ( z  =  { A }  \/  z  =  { A ,  B }
)  ->  E. x E. y  z  =  <. x ,  y >.
) )
8 jaob 800 . . . . . . . 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 >. )
) )
97, 8bitri 257 . . . . . . 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 >. )
) )
109albii 1699 . . . . . 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 >.
) ) )
11 19.26 1740 . . . . . 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 >. )
) )
1210, 11bitri 257 . . . . 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 >. )
) )
132, 12bitri 257 . . . 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 >.
) ) )
14 snex 4641 . . . . . . 7  |-  { A }  e.  _V
15 eqeq1 2475 . . . . . . . 8  |-  ( z  =  { A }  ->  ( z  =  { A }  <->  { A }  =  { A } ) )
16 eqeq1 2475 . . . . . . . . . 10  |-  ( z  =  { A }  ->  ( z  =  <. x ,  y >.  <->  { A }  =  <. x ,  y >. ) )
17 eqcom 2478 . . . . . . . . . . 11  |-  ( { A }  =  <. x ,  y >.  <->  <. x ,  y >.  =  { A } )
18 vex 3034 . . . . . . . . . . . 12  |-  x  e. 
_V
19 vex 3034 . . . . . . . . . . . 12  |-  y  e. 
_V
2018, 19, 3opeqsn 4697 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  =  { A }  <->  ( x  =  y  /\  A  =  { x } ) )
2117, 20bitri 257 . . . . . . . . . 10  |-  ( { A }  =  <. x ,  y >.  <->  ( x  =  y  /\  A  =  { x } ) )
2216, 21syl6bb 269 . . . . . . . . 9  |-  ( z  =  { A }  ->  ( z  =  <. x ,  y >.  <->  ( x  =  y  /\  A  =  { x } ) ) )
23222exbidv 1778 . . . . . . . 8  |-  ( z  =  { A }  ->  ( E. x E. y  z  =  <. x ,  y >.  <->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
2415, 23imbi12d 327 . . . . . . 7  |-  ( z  =  { A }  ->  ( ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  <->  ( { A }  =  { A }  ->  E. x E. y
( x  =  y  /\  A  =  {
x } ) ) ) )
2514, 24spcv 3126 . . . . . 6  |-  ( A. z ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  ->  ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
26 sneq 3969 . . . . . . . . 9  |-  ( w  =  x  ->  { w }  =  { x } )
2726eqeq2d 2481 . . . . . . . 8  |-  ( w  =  x  ->  ( A  =  { w } 
<->  A  =  { x } ) )
2827cbvexv 2130 . . . . . . 7  |-  ( E. w  A  =  {
w }  <->  E. x  A  =  { x } )
29 ax6evr 1867 . . . . . . . . 9  |-  E. y  x  =  y
30 19.41v 1838 . . . . . . . . 9  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
( E. y  x  =  y  /\  A  =  { x } ) )
3129, 30mpbiran 932 . . . . . . . 8  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
A  =  { x } )
3231exbii 1726 . . . . . . 7  |-  ( E. x E. y ( x  =  y  /\  A  =  { x } )  <->  E. x  A  =  { x } )
33 eqid 2471 . . . . . . . 8  |-  { A }  =  { A }
3433a1bi 344 . . . . . . 7  |-  ( E. x E. y ( x  =  y  /\  A  =  { x } )  <->  ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
3528, 32, 343bitr2ri 282 . . . . . 6  |-  ( ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) )  <->  E. w  A  =  { w } )
3625, 35sylib 201 . . . . 5  |-  ( A. z ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  ->  E. w  A  =  { w } )
37 eqid 2471 . . . . . 6  |-  { A ,  B }  =  { A ,  B }
38 prex 4642 . . . . . . 7  |-  { A ,  B }  e.  _V
39 eqeq1 2475 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( z  =  { A ,  B }  <->  { A ,  B }  =  { A ,  B } ) )
40 eqeq1 2475 . . . . . . . . 9  |-  ( z  =  { A ,  B }  ->  ( z  =  <. x ,  y
>. 
<->  { A ,  B }  =  <. x ,  y >. ) )
41402exbidv 1778 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( E. x E. y  z  =  <. x ,  y
>. 
<->  E. x E. y { A ,  B }  =  <. x ,  y
>. ) )
4239, 41imbi12d 327 . . . . . . 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
>. ) ) )
4338, 42spcv 3126 . . . . . 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
>. ) )
4437, 43mpi 20 . . . . 5  |-  ( A. z ( z  =  { A ,  B }  ->  E. x E. y 
z  =  <. x ,  y >. )  ->  E. x E. y { A ,  B }  =  <. x ,  y
>. )
45 eqcom 2478 . . . . . . . . . 10  |-  ( { A ,  B }  =  <. x ,  y
>. 
<-> 
<. x ,  y >.  =  { A ,  B } )
4618, 19, 3, 4opeqpr 4698 . . . . . . . . . 10  |-  ( <.
x ,  y >.  =  { A ,  B } 
<->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) ) )
4745, 46bitri 257 . . . . . . . . 9  |-  ( { A ,  B }  =  <. x ,  y
>. 
<->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) ) )
48 idd 24 . . . . . . . . . 10  |-  ( A  =  { w }  ->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
49 eqtr2 2491 . . . . . . . . . . . . . 14  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  { x ,  y }  =  { w } )
50 vex 3034 . . . . . . . . . . . . . . . 16  |-  w  e. 
_V
5118, 19, 50preqsn 4151 . . . . . . . . . . . . . . 15  |-  ( { x ,  y }  =  { w }  <->  ( x  =  y  /\  y  =  w )
)
5251simplbi 467 . . . . . . . . . . . . . 14  |-  ( { x ,  y }  =  { w }  ->  x  =  y )
5349, 52syl 17 . . . . . . . . . . . . 13  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  x  =  y )
54 dfsn2 3972 . . . . . . . . . . . . . . . . . . . 20  |-  { x }  =  { x ,  x }
55 preq2 4043 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  { x ,  x }  =  {
x ,  y } )
5654, 55syl5req 2518 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x ,  y }  =  { x } )
5756eqeq2d 2481 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( A  =  { x ,  y }  <->  A  =  { x } ) )
5854, 55syl5eq 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x }  =  { x ,  y } )
5958eqeq2d 2481 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( B  =  { x } 
<->  B  =  { x ,  y } ) )
6057, 59anbi12d 725 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
( A  =  {
x ,  y }  /\  B  =  {
x } )  <->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
6160biimpd 212 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
( A  =  {
x ,  y }  /\  B  =  {
x } )  -> 
( A  =  {
x }  /\  B  =  { x ,  y } ) ) )
6261expd 443 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  ( A  =  { x ,  y }  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) ) )
6362com12 31 . . . . . . . . . . . . . 14  |-  ( A  =  { x ,  y }  ->  (
x  =  y  -> 
( B  =  {
x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
6463adantr 472 . . . . . . . . . . . . 13  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  (
x  =  y  -> 
( B  =  {
x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
6553, 64mpd 15 . . . . . . . . . . . 12  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
6665expcom 442 . . . . . . . . . . 11  |-  ( A  =  { w }  ->  ( A  =  {
x ,  y }  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
6766impd 438 . . . . . . . . . 10  |-  ( A  =  { w }  ->  ( ( A  =  { x ,  y }  /\  B  =  { x } )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
6848, 67jaod 387 . . . . . . . . 9  |-  ( A  =  { w }  ->  ( ( ( A  =  { x }  /\  B  =  {
x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
6947, 68syl5bi 225 . . . . . . . 8  |-  ( A  =  { w }  ->  ( { A ,  B }  =  <. x ,  y >.  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) )
70692eximdv 1774 . . . . . . 7  |-  ( A  =  { w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y >.  ->  E. x E. y ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7170exlimiv 1784 . . . . . 6  |-  ( E. w  A  =  {
w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y
>.  ->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) ) )
7271imp 436 . . . . 5  |-  ( ( E. w  A  =  { w }  /\  E. x E. y { A ,  B }  =  <. x ,  y
>. )  ->  E. x E. y ( A  =  { x }  /\  B  =  { x ,  y } ) )
7336, 44, 72syl2an 485 . . . 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 } ) )
7413, 73sylbi 200 . . 3  |-  ( <. A ,  B >.  C_  ( _V  X.  _V )  ->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) )
75 simpr 468 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  { A } )
76 equid 1863 . . . . . . . . . . . . . 14  |-  x  =  x
7776jctl 550 . . . . . . . . . . . . 13  |-  ( A  =  { x }  ->  ( x  =  x  /\  A  =  {
x } ) )
7818, 18, 3opeqsn 4697 . . . . . . . . . . . . 13  |-  ( <.
x ,  x >.  =  { A }  <->  ( x  =  x  /\  A  =  { x } ) )
7977, 78sylibr 217 . . . . . . . . . . . 12  |-  ( A  =  { x }  -> 
<. x ,  x >.  =  { A } )
8079adantr 472 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  <. x ,  x >.  =  { A } )
8175, 80eqtr4d 2508 . . . . . . . . . 10  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  <. x ,  x >. )
82 opeq12 4160 . . . . . . . . . . . 12  |-  ( ( w  =  x  /\  v  =  x )  -> 
<. w ,  v >.  =  <. x ,  x >. )
8382eqeq2d 2481 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  x )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  x >. ) )
8418, 18, 83spc2ev 3128 . . . . . . . . . 10  |-  ( z  =  <. x ,  x >.  ->  E. w E. v 
z  =  <. w ,  v >. )
8581, 84syl 17 . . . . . . . . 9  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  E. w E. v  z  =  <. w ,  v >.
)
8685adantlr 729 . . . . . . . 8  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A } )  ->  E. w E. v 
z  =  <. w ,  v >. )
87 preq12 4044 . . . . . . . . . . . 12  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  { A ,  B }  =  { { x } ,  { x ,  y } } )
8887eqeq2d 2481 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( z  =  { A ,  B } 
<->  z  =  { {
x } ,  {
x ,  y } } ) )
8988biimpa 492 . . . . . . . . . 10  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  { { x } ,  { x ,  y } } )
9018, 19dfop 4157 . . . . . . . . . 10  |-  <. x ,  y >.  =  { { x } ,  { x ,  y } }
9189, 90syl6eqr 2523 . . . . . . . . 9  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  <. x ,  y
>. )
92 opeq12 4160 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  y )  -> 
<. w ,  v >.  =  <. x ,  y
>. )
9392eqeq2d 2481 . . . . . . . . . 10  |-  ( ( w  =  x  /\  v  =  y )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  y >.
) )
9418, 19, 93spc2ev 3128 . . . . . . . . 9  |-  ( z  =  <. x ,  y
>.  ->  E. w E. v 
z  =  <. w ,  v >. )
9591, 94syl 17 . . . . . . . 8  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  E. w E. v  z  =  <. w ,  v >.
)
9686, 95jaodan 802 . . . . . . 7  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  (
z  =  { A }  \/  z  =  { A ,  B }
) )  ->  E. w E. v  z  =  <. w ,  v >.
)
9796ex 441 . . . . . 6  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( (
z  =  { A }  \/  z  =  { A ,  B }
)  ->  E. w E. v  z  =  <. w ,  v >.
) )
98 elvv 4898 . . . . . 6  |-  ( z  e.  ( _V  X.  _V )  <->  E. w E. v 
z  =  <. w ,  v >. )
9997, 5, 983imtr4g 278 . . . . 5  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
) )
10099ssrdv 3424 . . . 4  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  <. A ,  B >.  C_  ( _V  X.  _V ) )
101100exlimivv 1786 . . 3  |-  ( E. x E. y ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  <. A ,  B >.  C_  ( _V  X.  _V ) )
10274, 101impbii 192 . 2  |-  ( <. A ,  B >.  C_  ( _V  X.  _V ) 
<->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) )
1031, 102bitri 257 1  |-  ( Rel 
<. A ,  B >.  <->  E. x E. y ( A  =  { x }  /\  B  =  {
x ,  y } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    \/ wo 375    /\ wa 376   A.wal 1450    = wceq 1452   E.wex 1671    e. wcel 1904   _Vcvv 3031    C_ wss 3390   {csn 3959   {cpr 3961   <.cop 3965    X. cxp 4837   Rel wrel 4844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-opab 4455  df-xp 4845  df-rel 4846
This theorem is referenced by:  funopg  5621
  Copyright terms: Public domain W3C validator