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

Theorem relop 5005
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 4861 . 2  |-  ( Rel 
<. A ,  B >.  <->  <. A ,  B >.  C_  ( _V  X.  _V ) )
2 dfss2 3459 . . . . 5  |-  ( <. A ,  B >.  C_  ( _V  X.  _V ) 
<-> 
A. z ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
) )
3 vex 3090 . . . . . . . . . 10  |-  z  e. 
_V
4 relop.1 . . . . . . . . . 10  |-  A  e. 
_V
5 relop.2 . . . . . . . . . 10  |-  B  e. 
_V
63, 4, 5elop 4688 . . . . . . . . 9  |-  ( z  e.  <. A ,  B >.  <-> 
( z  =  { A }  \/  z  =  { A ,  B } ) )
7 elvv 4913 . . . . . . . . 9  |-  ( z  e.  ( _V  X.  _V )  <->  E. x E. y 
z  =  <. x ,  y >. )
86, 7imbi12i 327 . . . . . . . 8  |-  ( ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
)  <->  ( ( z  =  { A }  \/  z  =  { A ,  B }
)  ->  E. x E. y  z  =  <. x ,  y >.
) )
9 jaob 790 . . . . . . . 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 >. )
) )
108, 9bitri 252 . . . . . . 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 >. )
) )
1110albii 1687 . . . . . 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 1727 . . . . . 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 >. )
) )
1311, 12bitri 252 . . . . 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 >. )
) )
142, 13bitri 252 . . . 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 snex 4663 . . . . . . 7  |-  { A }  e.  _V
16 eqeq1 2433 . . . . . . . 8  |-  ( z  =  { A }  ->  ( z  =  { A }  <->  { A }  =  { A } ) )
17 eqeq1 2433 . . . . . . . . . 10  |-  ( z  =  { A }  ->  ( z  =  <. x ,  y >.  <->  { A }  =  <. x ,  y >. ) )
18 eqcom 2438 . . . . . . . . . . 11  |-  ( { A }  =  <. x ,  y >.  <->  <. x ,  y >.  =  { A } )
19 vex 3090 . . . . . . . . . . . 12  |-  x  e. 
_V
20 vex 3090 . . . . . . . . . . . 12  |-  y  e. 
_V
2119, 20, 4opeqsn 4717 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  =  { A }  <->  ( x  =  y  /\  A  =  { x } ) )
2218, 21bitri 252 . . . . . . . . . 10  |-  ( { A }  =  <. x ,  y >.  <->  ( x  =  y  /\  A  =  { x } ) )
2317, 22syl6bb 264 . . . . . . . . 9  |-  ( z  =  { A }  ->  ( z  =  <. x ,  y >.  <->  ( x  =  y  /\  A  =  { x } ) ) )
24232exbidv 1763 . . . . . . . 8  |-  ( z  =  { A }  ->  ( E. x E. y  z  =  <. x ,  y >.  <->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
2516, 24imbi12d 321 . . . . . . 7  |-  ( z  =  { A }  ->  ( ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  <->  ( { A }  =  { A }  ->  E. x E. y
( x  =  y  /\  A  =  {
x } ) ) ) )
2615, 25spcv 3178 . . . . . 6  |-  ( A. z ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  ->  ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
27 sneq 4012 . . . . . . . . 9  |-  ( w  =  x  ->  { w }  =  { x } )
2827eqeq2d 2443 . . . . . . . 8  |-  ( w  =  x  ->  ( A  =  { w } 
<->  A  =  { x } ) )
2928cbvexv 2080 . . . . . . 7  |-  ( E. w  A  =  {
w }  <->  E. x  A  =  { x } )
30 ax6ev 1799 . . . . . . . . . 10  |-  E. y 
y  =  x
31 equcom 1846 . . . . . . . . . . 11  |-  ( y  =  x  <->  x  =  y )
3231exbii 1714 . . . . . . . . . 10  |-  ( E. y  y  =  x  <->  E. y  x  =  y )
3330, 32mpbi 211 . . . . . . . . 9  |-  E. y  x  =  y
34 19.41v 1822 . . . . . . . . 9  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
( E. y  x  =  y  /\  A  =  { x } ) )
3533, 34mpbiran 926 . . . . . . . 8  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
A  =  { x } )
3635exbii 1714 . . . . . . 7  |-  ( E. x E. y ( x  =  y  /\  A  =  { x } )  <->  E. x  A  =  { x } )
37 eqid 2429 . . . . . . . 8  |-  { A }  =  { A }
3837a1bi 338 . . . . . . 7  |-  ( E. x E. y ( x  =  y  /\  A  =  { x } )  <->  ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
3929, 36, 383bitr2ri 277 . . . . . 6  |-  ( ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) )  <->  E. w  A  =  { w } )
4026, 39sylib 199 . . . . 5  |-  ( A. z ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  ->  E. w  A  =  { w } )
41 eqid 2429 . . . . . 6  |-  { A ,  B }  =  { A ,  B }
42 prex 4664 . . . . . . 7  |-  { A ,  B }  e.  _V
43 eqeq1 2433 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( z  =  { A ,  B }  <->  { A ,  B }  =  { A ,  B } ) )
44 eqeq1 2433 . . . . . . . . 9  |-  ( z  =  { A ,  B }  ->  ( z  =  <. x ,  y
>. 
<->  { A ,  B }  =  <. x ,  y >. ) )
45442exbidv 1763 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( E. x E. y  z  =  <. x ,  y
>. 
<->  E. x E. y { A ,  B }  =  <. x ,  y
>. ) )
4643, 45imbi12d 321 . . . . . . 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
>. ) ) )
4742, 46spcv 3178 . . . . . 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
>. ) )
4841, 47mpi 21 . . . . 5  |-  ( A. z ( z  =  { A ,  B }  ->  E. x E. y 
z  =  <. x ,  y >. )  ->  E. x E. y { A ,  B }  =  <. x ,  y
>. )
49 eqcom 2438 . . . . . . . . . 10  |-  ( { A ,  B }  =  <. x ,  y
>. 
<-> 
<. x ,  y >.  =  { A ,  B } )
5019, 20, 4, 5opeqpr 4718 . . . . . . . . . 10  |-  ( <.
x ,  y >.  =  { A ,  B } 
<->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) ) )
5149, 50bitri 252 . . . . . . . . 9  |-  ( { A ,  B }  =  <. x ,  y
>. 
<->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) ) )
52 idd 25 . . . . . . . . . 10  |-  ( A  =  { w }  ->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
53 eqtr2 2456 . . . . . . . . . . . . . 14  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  { x ,  y }  =  { w } )
54 vex 3090 . . . . . . . . . . . . . . . 16  |-  w  e. 
_V
5519, 20, 54preqsn 4186 . . . . . . . . . . . . . . 15  |-  ( { x ,  y }  =  { w }  <->  ( x  =  y  /\  y  =  w )
)
5655simplbi 461 . . . . . . . . . . . . . 14  |-  ( { x ,  y }  =  { w }  ->  x  =  y )
5753, 56syl 17 . . . . . . . . . . . . 13  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  x  =  y )
58 dfsn2 4015 . . . . . . . . . . . . . . . . . . . 20  |-  { x }  =  { x ,  x }
59 preq2 4083 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  { x ,  x }  =  {
x ,  y } )
6058, 59syl5req 2483 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x ,  y }  =  { x } )
6160eqeq2d 2443 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( A  =  { x ,  y }  <->  A  =  { x } ) )
6258, 59syl5eq 2482 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x }  =  { x ,  y } )
6362eqeq2d 2443 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( B  =  { x } 
<->  B  =  { x ,  y } ) )
6461, 63anbi12d 715 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
( A  =  {
x ,  y }  /\  B  =  {
x } )  <->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
6564biimpd 210 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
( A  =  {
x ,  y }  /\  B  =  {
x } )  -> 
( A  =  {
x }  /\  B  =  { x ,  y } ) ) )
6665expd 437 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  ( A  =  { x ,  y }  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) ) )
6766com12 32 . . . . . . . . . . . . . 14  |-  ( A  =  { x ,  y }  ->  (
x  =  y  -> 
( B  =  {
x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
6867adantr 466 . . . . . . . . . . . . 13  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  (
x  =  y  -> 
( B  =  {
x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
6957, 68mpd 15 . . . . . . . . . . . 12  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7069expcom 436 . . . . . . . . . . 11  |-  ( A  =  { w }  ->  ( A  =  {
x ,  y }  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
7170impd 432 . . . . . . . . . 10  |-  ( A  =  { w }  ->  ( ( A  =  { x ,  y }  /\  B  =  { x } )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7252, 71jaod 381 . . . . . . . . 9  |-  ( A  =  { w }  ->  ( ( ( A  =  { x }  /\  B  =  {
x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7351, 72syl5bi 220 . . . . . . . 8  |-  ( A  =  { w }  ->  ( { A ,  B }  =  <. x ,  y >.  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) )
74732eximdv 1759 . . . . . . 7  |-  ( A  =  { w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y >.  ->  E. x E. y ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7574exlimiv 1769 . . . . . 6  |-  ( E. w  A  =  {
w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y
>.  ->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) ) )
7675imp 430 . . . . 5  |-  ( ( E. w  A  =  { w }  /\  E. x E. y { A ,  B }  =  <. x ,  y
>. )  ->  E. x E. y ( A  =  { x }  /\  B  =  { x ,  y } ) )
7740, 48, 76syl2an 479 . . . 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 } ) )
7814, 77sylbi 198 . . 3  |-  ( <. A ,  B >.  C_  ( _V  X.  _V )  ->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) )
79 simpr 462 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  { A } )
80 equid 1842 . . . . . . . . . . . . . 14  |-  x  =  x
8180jctl 543 . . . . . . . . . . . . 13  |-  ( A  =  { x }  ->  ( x  =  x  /\  A  =  {
x } ) )
8219, 19, 4opeqsn 4717 . . . . . . . . . . . . 13  |-  ( <.
x ,  x >.  =  { A }  <->  ( x  =  x  /\  A  =  { x } ) )
8381, 82sylibr 215 . . . . . . . . . . . 12  |-  ( A  =  { x }  -> 
<. x ,  x >.  =  { A } )
8483adantr 466 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  <. x ,  x >.  =  { A } )
8579, 84eqtr4d 2473 . . . . . . . . . 10  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  <. x ,  x >. )
86 opeq12 4192 . . . . . . . . . . . 12  |-  ( ( w  =  x  /\  v  =  x )  -> 
<. w ,  v >.  =  <. x ,  x >. )
8786eqeq2d 2443 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  x )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  x >. ) )
8819, 19, 87spc2ev 3180 . . . . . . . . . 10  |-  ( z  =  <. x ,  x >.  ->  E. w E. v 
z  =  <. w ,  v >. )
8985, 88syl 17 . . . . . . . . 9  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  E. w E. v  z  =  <. w ,  v >.
)
9089adantlr 719 . . . . . . . 8  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A } )  ->  E. w E. v 
z  =  <. w ,  v >. )
91 preq12 4084 . . . . . . . . . . . 12  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  { A ,  B }  =  { { x } ,  { x ,  y } } )
9291eqeq2d 2443 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( z  =  { A ,  B } 
<->  z  =  { {
x } ,  {
x ,  y } } ) )
9392biimpa 486 . . . . . . . . . 10  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  { { x } ,  { x ,  y } } )
9419, 20dfop 4189 . . . . . . . . . 10  |-  <. x ,  y >.  =  { { x } ,  { x ,  y } }
9593, 94syl6eqr 2488 . . . . . . . . 9  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  <. x ,  y
>. )
96 opeq12 4192 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  y )  -> 
<. w ,  v >.  =  <. x ,  y
>. )
9796eqeq2d 2443 . . . . . . . . . 10  |-  ( ( w  =  x  /\  v  =  y )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  y >.
) )
9819, 20, 97spc2ev 3180 . . . . . . . . 9  |-  ( z  =  <. x ,  y
>.  ->  E. w E. v 
z  =  <. w ,  v >. )
9995, 98syl 17 . . . . . . . 8  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  E. w E. v  z  =  <. w ,  v >.
)
10090, 99jaodan 792 . . . . . . 7  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  (
z  =  { A }  \/  z  =  { A ,  B }
) )  ->  E. w E. v  z  =  <. w ,  v >.
)
101100ex 435 . . . . . 6  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( (
z  =  { A }  \/  z  =  { A ,  B }
)  ->  E. w E. v  z  =  <. w ,  v >.
) )
102 elvv 4913 . . . . . 6  |-  ( z  e.  ( _V  X.  _V )  <->  E. w E. v 
z  =  <. w ,  v >. )
103101, 6, 1023imtr4g 273 . . . . 5  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
) )
104103ssrdv 3476 . . . 4  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  <. A ,  B >.  C_  ( _V  X.  _V ) )
105104exlimivv 1770 . . 3  |-  ( E. x E. y ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  <. A ,  B >.  C_  ( _V  X.  _V ) )
10678, 105impbii 190 . 2  |-  ( <. A ,  B >.  C_  ( _V  X.  _V ) 
<->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) )
1071, 106bitri 252 1  |-  ( Rel 
<. A ,  B >.  <->  E. x E. y ( A  =  { x }  /\  B  =  {
x ,  y } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370   A.wal 1435    = wceq 1437   E.wex 1659    e. wcel 1870   _Vcvv 3087    C_ wss 3442   {csn 4002   {cpr 4004   <.cop 4008    X. cxp 4852   Rel wrel 4859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-opab 4485  df-xp 4860  df-rel 4861
This theorem is referenced by:  funopg  5633
  Copyright terms: Public domain W3C validator