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

Theorem relop 5066
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 4920 . 2  |-  ( Rel 
<. A ,  B >.  <->  <. A ,  B >.  C_  ( _V  X.  _V ) )
2 dfss2 3406 . . . . 5  |-  ( <. A ,  B >.  C_  ( _V  X.  _V ) 
<-> 
A. z ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
) )
3 vex 3037 . . . . . . . . . 10  |-  z  e. 
_V
4 relop.1 . . . . . . . . . 10  |-  A  e. 
_V
5 relop.2 . . . . . . . . . 10  |-  B  e. 
_V
63, 4, 5elop 4628 . . . . . . . . 9  |-  ( z  e.  <. A ,  B >.  <-> 
( z  =  { A }  \/  z  =  { A ,  B } ) )
7 elvv 4972 . . . . . . . . 9  |-  ( z  e.  ( _V  X.  _V )  <->  E. x E. y 
z  =  <. x ,  y >. )
86, 7imbi12i 324 . . . . . . . 8  |-  ( ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
)  <->  ( ( z  =  { A }  \/  z  =  { A ,  B }
)  ->  E. x E. y  z  =  <. x ,  y >.
) )
9 jaob 781 . . . . . . . 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 249 . . . . . . 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 1648 . . . . . 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 1688 . . . . . 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 249 . . . . 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 249 . . . 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 4603 . . . . . . 7  |-  { A }  e.  _V
16 eqeq1 2386 . . . . . . . 8  |-  ( z  =  { A }  ->  ( z  =  { A }  <->  { A }  =  { A } ) )
17 eqeq1 2386 . . . . . . . . . 10  |-  ( z  =  { A }  ->  ( z  =  <. x ,  y >.  <->  { A }  =  <. x ,  y >. ) )
18 eqcom 2391 . . . . . . . . . . 11  |-  ( { A }  =  <. x ,  y >.  <->  <. x ,  y >.  =  { A } )
19 vex 3037 . . . . . . . . . . . 12  |-  x  e. 
_V
20 vex 3037 . . . . . . . . . . . 12  |-  y  e. 
_V
2119, 20, 4opeqsn 4657 . . . . . . . . . . 11  |-  ( <.
x ,  y >.  =  { A }  <->  ( x  =  y  /\  A  =  { x } ) )
2218, 21bitri 249 . . . . . . . . . 10  |-  ( { A }  =  <. x ,  y >.  <->  ( x  =  y  /\  A  =  { x } ) )
2317, 22syl6bb 261 . . . . . . . . 9  |-  ( z  =  { A }  ->  ( z  =  <. x ,  y >.  <->  ( x  =  y  /\  A  =  { x } ) ) )
24232exbidv 1724 . . . . . . . 8  |-  ( z  =  { A }  ->  ( E. x E. y  z  =  <. x ,  y >.  <->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
2516, 24imbi12d 318 . . . . . . 7  |-  ( z  =  { A }  ->  ( ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  <->  ( { A }  =  { A }  ->  E. x E. y
( x  =  y  /\  A  =  {
x } ) ) ) )
2615, 25spcv 3125 . . . . . 6  |-  ( A. z ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  ->  ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
27 sneq 3954 . . . . . . . . 9  |-  ( w  =  x  ->  { w }  =  { x } )
2827eqeq2d 2396 . . . . . . . 8  |-  ( w  =  x  ->  ( A  =  { w } 
<->  A  =  { x } ) )
2928cbvexv 2031 . . . . . . 7  |-  ( E. w  A  =  {
w }  <->  E. x  A  =  { x } )
30 ax6ev 1757 . . . . . . . . . 10  |-  E. y 
y  =  x
31 equcom 1802 . . . . . . . . . . 11  |-  ( y  =  x  <->  x  =  y )
3231exbii 1675 . . . . . . . . . 10  |-  ( E. y  y  =  x  <->  E. y  x  =  y )
3330, 32mpbi 208 . . . . . . . . 9  |-  E. y  x  =  y
34 19.41v 1779 . . . . . . . . 9  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
( E. y  x  =  y  /\  A  =  { x } ) )
3533, 34mpbiran 916 . . . . . . . 8  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
A  =  { x } )
3635exbii 1675 . . . . . . 7  |-  ( E. x E. y ( x  =  y  /\  A  =  { x } )  <->  E. x  A  =  { x } )
37 eqid 2382 . . . . . . . 8  |-  { A }  =  { A }
3837a1bi 335 . . . . . . 7  |-  ( E. x E. y ( x  =  y  /\  A  =  { x } )  <->  ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
3929, 36, 383bitr2ri 274 . . . . . 6  |-  ( ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) )  <->  E. w  A  =  { w } )
4026, 39sylib 196 . . . . 5  |-  ( A. z ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  ->  E. w  A  =  { w } )
41 eqid 2382 . . . . . 6  |-  { A ,  B }  =  { A ,  B }
42 prex 4604 . . . . . . 7  |-  { A ,  B }  e.  _V
43 eqeq1 2386 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( z  =  { A ,  B }  <->  { A ,  B }  =  { A ,  B } ) )
44 eqeq1 2386 . . . . . . . . 9  |-  ( z  =  { A ,  B }  ->  ( z  =  <. x ,  y
>. 
<->  { A ,  B }  =  <. x ,  y >. ) )
45442exbidv 1724 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( E. x E. y  z  =  <. x ,  y
>. 
<->  E. x E. y { A ,  B }  =  <. x ,  y
>. ) )
4643, 45imbi12d 318 . . . . . . 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 3125 . . . . . 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 17 . . . . 5  |-  ( A. z ( z  =  { A ,  B }  ->  E. x E. y 
z  =  <. x ,  y >. )  ->  E. x E. y { A ,  B }  =  <. x ,  y
>. )
49 eqcom 2391 . . . . . . . . . 10  |-  ( { A ,  B }  =  <. x ,  y
>. 
<-> 
<. x ,  y >.  =  { A ,  B } )
5019, 20, 4, 5opeqpr 4658 . . . . . . . . . 10  |-  ( <.
x ,  y >.  =  { A ,  B } 
<->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) ) )
5149, 50bitri 249 . . . . . . . . 9  |-  ( { A ,  B }  =  <. x ,  y
>. 
<->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) ) )
52 idd 24 . . . . . . . . . 10  |-  ( A  =  { w }  ->  ( ( A  =  { x }  /\  B  =  { x ,  y } )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
53 eqtr2 2409 . . . . . . . . . . . . . 14  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  { x ,  y }  =  { w } )
54 vex 3037 . . . . . . . . . . . . . . . 16  |-  w  e. 
_V
5519, 20, 54preqsn 4127 . . . . . . . . . . . . . . 15  |-  ( { x ,  y }  =  { w }  <->  ( x  =  y  /\  y  =  w )
)
5655simplbi 458 . . . . . . . . . . . . . 14  |-  ( { x ,  y }  =  { w }  ->  x  =  y )
5753, 56syl 16 . . . . . . . . . . . . 13  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  x  =  y )
58 dfsn2 3957 . . . . . . . . . . . . . . . . . . . 20  |-  { x }  =  { x ,  x }
59 preq2 4024 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  { x ,  x }  =  {
x ,  y } )
6058, 59syl5req 2436 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x ,  y }  =  { x } )
6160eqeq2d 2396 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( A  =  { x ,  y }  <->  A  =  { x } ) )
6258, 59syl5eq 2435 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x }  =  { x ,  y } )
6362eqeq2d 2396 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( B  =  { x } 
<->  B  =  { x ,  y } ) )
6461, 63anbi12d 708 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  (
( A  =  {
x ,  y }  /\  B  =  {
x } )  <->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
6564biimpd 207 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  (
( A  =  {
x ,  y }  /\  B  =  {
x } )  -> 
( A  =  {
x }  /\  B  =  { x ,  y } ) ) )
6665expd 434 . . . . . . . . . . . . . . 15  |-  ( x  =  y  ->  ( A  =  { x ,  y }  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) ) )
6766com12 31 . . . . . . . . . . . . . 14  |-  ( A  =  { x ,  y }  ->  (
x  =  y  -> 
( B  =  {
x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
6867adantr 463 . . . . . . . . . . . . 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 433 . . . . . . . . . . 11  |-  ( A  =  { w }  ->  ( A  =  {
x ,  y }  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
7170impd 429 . . . . . . . . . 10  |-  ( A  =  { w }  ->  ( ( A  =  { x ,  y }  /\  B  =  { x } )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7252, 71jaod 378 . . . . . . . . 9  |-  ( A  =  { w }  ->  ( ( ( A  =  { x }  /\  B  =  {
x ,  y } )  \/  ( A  =  { x ,  y }  /\  B  =  { x } ) )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7351, 72syl5bi 217 . . . . . . . 8  |-  ( A  =  { w }  ->  ( { A ,  B }  =  <. x ,  y >.  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) )
74732eximdv 1720 . . . . . . 7  |-  ( A  =  { w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y >.  ->  E. x E. y ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7574exlimiv 1730 . . . . . 6  |-  ( E. w  A  =  {
w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y
>.  ->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) ) )
7675imp 427 . . . . 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 475 . . . 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 195 . . 3  |-  ( <. A ,  B >.  C_  ( _V  X.  _V )  ->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) )
79 simpr 459 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  { A } )
80 equid 1799 . . . . . . . . . . . . . 14  |-  x  =  x
8180jctl 539 . . . . . . . . . . . . 13  |-  ( A  =  { x }  ->  ( x  =  x  /\  A  =  {
x } ) )
8219, 19, 4opeqsn 4657 . . . . . . . . . . . . 13  |-  ( <.
x ,  x >.  =  { A }  <->  ( x  =  x  /\  A  =  { x } ) )
8381, 82sylibr 212 . . . . . . . . . . . 12  |-  ( A  =  { x }  -> 
<. x ,  x >.  =  { A } )
8483adantr 463 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  <. x ,  x >.  =  { A } )
8579, 84eqtr4d 2426 . . . . . . . . . 10  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  <. x ,  x >. )
86 opeq12 4133 . . . . . . . . . . . 12  |-  ( ( w  =  x  /\  v  =  x )  -> 
<. w ,  v >.  =  <. x ,  x >. )
8786eqeq2d 2396 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  x )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  x >. ) )
8819, 19, 87spc2ev 3127 . . . . . . . . . 10  |-  ( z  =  <. x ,  x >.  ->  E. w E. v 
z  =  <. w ,  v >. )
8985, 88syl 16 . . . . . . . . 9  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  E. w E. v  z  =  <. w ,  v >.
)
9089adantlr 712 . . . . . . . 8  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A } )  ->  E. w E. v 
z  =  <. w ,  v >. )
91 preq12 4025 . . . . . . . . . . . 12  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  { A ,  B }  =  { { x } ,  { x ,  y } } )
9291eqeq2d 2396 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( z  =  { A ,  B } 
<->  z  =  { {
x } ,  {
x ,  y } } ) )
9392biimpa 482 . . . . . . . . . 10  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  { { x } ,  { x ,  y } } )
9419, 20dfop 4130 . . . . . . . . . 10  |-  <. x ,  y >.  =  { { x } ,  { x ,  y } }
9593, 94syl6eqr 2441 . . . . . . . . 9  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  <. x ,  y
>. )
96 opeq12 4133 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  y )  -> 
<. w ,  v >.  =  <. x ,  y
>. )
9796eqeq2d 2396 . . . . . . . . . 10  |-  ( ( w  =  x  /\  v  =  y )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  y >.
) )
9819, 20, 97spc2ev 3127 . . . . . . . . 9  |-  ( z  =  <. x ,  y
>.  ->  E. w E. v 
z  =  <. w ,  v >. )
9995, 98syl 16 . . . . . . . 8  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  E. w E. v  z  =  <. w ,  v >.
)
10090, 99jaodan 783 . . . . . . 7  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  (
z  =  { A }  \/  z  =  { A ,  B }
) )  ->  E. w E. v  z  =  <. w ,  v >.
)
101100ex 432 . . . . . 6  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( (
z  =  { A }  \/  z  =  { A ,  B }
)  ->  E. w E. v  z  =  <. w ,  v >.
) )
102 elvv 4972 . . . . . 6  |-  ( z  e.  ( _V  X.  _V )  <->  E. w E. v 
z  =  <. w ,  v >. )
103101, 6, 1023imtr4g 270 . . . . 5  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
) )
104103ssrdv 3423 . . . 4  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  <. A ,  B >.  C_  ( _V  X.  _V ) )
105104exlimivv 1731 . . 3  |-  ( E. x E. y ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  <. A ,  B >.  C_  ( _V  X.  _V ) )
10678, 105impbii 188 . 2  |-  ( <. A ,  B >.  C_  ( _V  X.  _V ) 
<->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) )
1071, 106bitri 249 1  |-  ( Rel 
<. A ,  B >.  <->  E. x E. y ( A  =  { x }  /\  B  =  {
x ,  y } ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 366    /\ wa 367   A.wal 1397    = wceq 1399   E.wex 1620    e. wcel 1826   _Vcvv 3034    C_ wss 3389   {csn 3944   {cpr 3946   <.cop 3950    X. cxp 4911   Rel wrel 4918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-opab 4426  df-xp 4919  df-rel 4920
This theorem is referenced by:  funopg  5528
  Copyright terms: Public domain W3C validator