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

Theorem relop 4985
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 4841 . 2  |-  ( Rel 
<. A ,  B >.  <->  <. A ,  B >.  C_  ( _V  X.  _V ) )
2 dfss2 3421 . . . . 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 4893 . . . . . . . . 9  |-  ( z  e.  ( _V  X.  _V )  <->  E. x E. y 
z  =  <. x ,  y >. )
75, 6imbi12i 328 . . . . . . . 8  |-  ( ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
)  <->  ( ( z  =  { A }  \/  z  =  { A ,  B }
)  ->  E. x E. y  z  =  <. x ,  y >.
) )
8 jaob 792 . . . . . . . 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 253 . . . . . . 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 1691 . . . . . 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 1732 . . . . . 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 253 . . . . 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 253 . . . 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 2455 . . . . . . . 8  |-  ( z  =  { A }  ->  ( z  =  { A }  <->  { A }  =  { A } ) )
16 eqeq1 2455 . . . . . . . . . 10  |-  ( z  =  { A }  ->  ( z  =  <. x ,  y >.  <->  { A }  =  <. x ,  y >. ) )
17 eqcom 2458 . . . . . . . . . . 11  |-  ( { A }  =  <. x ,  y >.  <->  <. x ,  y >.  =  { A } )
18 vex 3048 . . . . . . . . . . . 12  |-  x  e. 
_V
19 vex 3048 . . . . . . . . . . . 12  |-  y  e. 
_V
2018, 19, 3opeqsn 4697 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  =  { A }  <->  ( x  =  y  /\  A  =  { x } ) )
2117, 20bitri 253 . . . . . . . . . 10  |-  ( { A }  =  <. x ,  y >.  <->  ( x  =  y  /\  A  =  { x } ) )
2216, 21syl6bb 265 . . . . . . . . 9  |-  ( z  =  { A }  ->  ( z  =  <. x ,  y >.  <->  ( x  =  y  /\  A  =  { x } ) ) )
23222exbidv 1770 . . . . . . . 8  |-  ( z  =  { A }  ->  ( E. x E. y  z  =  <. x ,  y >.  <->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
2415, 23imbi12d 322 . . . . . . 7  |-  ( z  =  { A }  ->  ( ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  <->  ( { A }  =  { A }  ->  E. x E. y
( x  =  y  /\  A  =  {
x } ) ) ) )
2514, 24spcv 3140 . . . . . 6  |-  ( A. z ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  ->  ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
26 sneq 3978 . . . . . . . . 9  |-  ( w  =  x  ->  { w }  =  { x } )
2726eqeq2d 2461 . . . . . . . 8  |-  ( w  =  x  ->  ( A  =  { w } 
<->  A  =  { x } ) )
2827cbvexv 2117 . . . . . . 7  |-  ( E. w  A  =  {
w }  <->  E. x  A  =  { x } )
29 ax6evr 1859 . . . . . . . . 9  |-  E. y  x  =  y
30 19.41v 1830 . . . . . . . . 9  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
( E. y  x  =  y  /\  A  =  { x } ) )
3129, 30mpbiran 929 . . . . . . . 8  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
A  =  { x } )
3231exbii 1718 . . . . . . 7  |-  ( E. x E. y ( x  =  y  /\  A  =  { x } )  <->  E. x  A  =  { x } )
33 eqid 2451 . . . . . . . 8  |-  { A }  =  { A }
3433a1bi 339 . . . . . . 7  |-  ( E. x E. y ( x  =  y  /\  A  =  { x } )  <->  ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
3528, 32, 343bitr2ri 278 . . . . . 6  |-  ( ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) )  <->  E. w  A  =  { w } )
3625, 35sylib 200 . . . . 5  |-  ( A. z ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  ->  E. w  A  =  { w } )
37 eqid 2451 . . . . . 6  |-  { A ,  B }  =  { A ,  B }
38 prex 4642 . . . . . . 7  |-  { A ,  B }  e.  _V
39 eqeq1 2455 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( z  =  { A ,  B }  <->  { A ,  B }  =  { A ,  B } ) )
40 eqeq1 2455 . . . . . . . . 9  |-  ( z  =  { A ,  B }  ->  ( z  =  <. x ,  y
>. 
<->  { A ,  B }  =  <. x ,  y >. ) )
41402exbidv 1770 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( E. x E. y  z  =  <. x ,  y
>. 
<->  E. x E. y { A ,  B }  =  <. x ,  y
>. ) )
4239, 41imbi12d 322 . . . . . . 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 3140 . . . . . 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 2458 . . . . . . . . . 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 253 . . . . . . . . 9  |-  ( { A ,  B }  =  <. x ,  y
>. 
<->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) ) )
48 idd 25 . . . . . . . . . 10  |-  ( A  =  { w }  ->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
49 eqtr2 2471 . . . . . . . . . . . . . 14  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  { x ,  y }  =  { w } )
50 vex 3048 . . . . . . . . . . . . . . . 16  |-  w  e. 
_V
5118, 19, 50preqsn 4159 . . . . . . . . . . . . . . 15  |-  ( { x ,  y }  =  { w }  <->  ( x  =  y  /\  y  =  w )
)
5251simplbi 462 . . . . . . . . . . . . . 14  |-  ( { x ,  y }  =  { w }  ->  x  =  y )
5349, 52syl 17 . . . . . . . . . . . . 13  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  x  =  y )
54 dfsn2 3981 . . . . . . . . . . . . . . . . . . . 20  |-  { x }  =  { x ,  x }
55 preq2 4052 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  { x ,  x }  =  {
x ,  y } )
5654, 55syl5req 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x ,  y }  =  { x } )
5756eqeq2d 2461 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( A  =  { x ,  y }  <->  A  =  { x } ) )
5854, 55syl5eq 2497 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x }  =  { x ,  y } )
5958eqeq2d 2461 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( B  =  { x } 
<->  B  =  { x ,  y } ) )
6057, 59anbi12d 717 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
( A  =  {
x ,  y }  /\  B  =  {
x } )  <->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
6160biimpd 211 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
( A  =  {
x ,  y }  /\  B  =  {
x } )  -> 
( A  =  {
x }  /\  B  =  { x ,  y } ) ) )
6261expd 438 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  ( A  =  { x ,  y }  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) ) )
6362com12 32 . . . . . . . . . . . . . 14  |-  ( A  =  { x ,  y }  ->  (
x  =  y  -> 
( B  =  {
x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
6463adantr 467 . . . . . . . . . . . . 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 437 . . . . . . . . . . 11  |-  ( A  =  { w }  ->  ( A  =  {
x ,  y }  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
6766impd 433 . . . . . . . . . 10  |-  ( A  =  { w }  ->  ( ( A  =  { x ,  y }  /\  B  =  { x } )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
6848, 67jaod 382 . . . . . . . . 9  |-  ( A  =  { w }  ->  ( ( ( A  =  { x }  /\  B  =  {
x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
6947, 68syl5bi 221 . . . . . . . 8  |-  ( A  =  { w }  ->  ( { A ,  B }  =  <. x ,  y >.  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) )
70692eximdv 1766 . . . . . . 7  |-  ( A  =  { w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y >.  ->  E. x E. y ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7170exlimiv 1776 . . . . . 6  |-  ( E. w  A  =  {
w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y
>.  ->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) ) )
7271imp 431 . . . . 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 480 . . . 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 199 . . 3  |-  ( <. A ,  B >.  C_  ( _V  X.  _V )  ->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) )
75 simpr 463 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  { A } )
76 equid 1855 . . . . . . . . . . . . . 14  |-  x  =  x
7776jctl 544 . . . . . . . . . . . . 13  |-  ( A  =  { x }  ->  ( x  =  x  /\  A  =  {
x } ) )
7818, 18, 3opeqsn 4697 . . . . . . . . . . . . 13  |-  ( <.
x ,  x >.  =  { A }  <->  ( x  =  x  /\  A  =  { x } ) )
7977, 78sylibr 216 . . . . . . . . . . . 12  |-  ( A  =  { x }  -> 
<. x ,  x >.  =  { A } )
8079adantr 467 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  <. x ,  x >.  =  { A } )
8175, 80eqtr4d 2488 . . . . . . . . . 10  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  <. x ,  x >. )
82 opeq12 4168 . . . . . . . . . . . 12  |-  ( ( w  =  x  /\  v  =  x )  -> 
<. w ,  v >.  =  <. x ,  x >. )
8382eqeq2d 2461 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  x )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  x >. ) )
8418, 18, 83spc2ev 3142 . . . . . . . . . 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 721 . . . . . . . 8  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A } )  ->  E. w E. v 
z  =  <. w ,  v >. )
87 preq12 4053 . . . . . . . . . . . 12  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  { A ,  B }  =  { { x } ,  { x ,  y } } )
8887eqeq2d 2461 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( z  =  { A ,  B } 
<->  z  =  { {
x } ,  {
x ,  y } } ) )
8988biimpa 487 . . . . . . . . . 10  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  { { x } ,  { x ,  y } } )
9018, 19dfop 4165 . . . . . . . . . 10  |-  <. x ,  y >.  =  { { x } ,  { x ,  y } }
9189, 90syl6eqr 2503 . . . . . . . . 9  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  <. x ,  y
>. )
92 opeq12 4168 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  y )  -> 
<. w ,  v >.  =  <. x ,  y
>. )
9392eqeq2d 2461 . . . . . . . . . 10  |-  ( ( w  =  x  /\  v  =  y )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  y >.
) )
9418, 19, 93spc2ev 3142 . . . . . . . . 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 794 . . . . . . 7  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  (
z  =  { A }  \/  z  =  { A ,  B }
) )  ->  E. w E. v  z  =  <. w ,  v >.
)
9796ex 436 . . . . . 6  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( (
z  =  { A }  \/  z  =  { A ,  B }
)  ->  E. w E. v  z  =  <. w ,  v >.
) )
98 elvv 4893 . . . . . 6  |-  ( z  e.  ( _V  X.  _V )  <->  E. w E. v 
z  =  <. w ,  v >. )
9997, 5, 983imtr4g 274 . . . . 5  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
) )
10099ssrdv 3438 . . . 4  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  <. A ,  B >.  C_  ( _V  X.  _V ) )
101100exlimivv 1778 . . 3  |-  ( E. x E. y ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  <. A ,  B >.  C_  ( _V  X.  _V ) )
10274, 101impbii 191 . 2  |-  ( <. A ,  B >.  C_  ( _V  X.  _V ) 
<->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) )
1031, 102bitri 253 1  |-  ( Rel 
<. A ,  B >.  <->  E. x E. y ( A  =  { x }  /\  B  =  {
x ,  y } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    \/ wo 370    /\ wa 371   A.wal 1442    = wceq 1444   E.wex 1663    e. wcel 1887   _Vcvv 3045    C_ wss 3404   {csn 3968   {cpr 3970   <.cop 3974    X. cxp 4832   Rel wrel 4839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-opab 4462  df-xp 4840  df-rel 4841
This theorem is referenced by:  funopg  5614
  Copyright terms: Public domain W3C validator