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

Theorem relop 4989
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 3344 . . . . 5  |-  ( <. A ,  B >.  C_  ( _V  X.  _V ) 
<-> 
A. z ( z  e.  <. A ,  B >.  ->  z  e.  ( _V  X.  _V )
) )
3 vex 2974 . . . . . . . . . 10  |-  z  e. 
_V
4 relop.1 . . . . . . . . . 10  |-  A  e. 
_V
5 relop.2 . . . . . . . . . 10  |-  B  e. 
_V
63, 4, 5elop 4557 . . . . . . . . 9  |-  ( z  e.  <. A ,  B >.  <-> 
( z  =  { A }  \/  z  =  { A ,  B } ) )
7 elvv 4896 . . . . . . . . 9  |-  ( z  e.  ( _V  X.  _V )  <->  E. x E. y 
z  =  <. x ,  y >. )
86, 7imbi12i 326 . . . . . . . 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 1610 . . . . . 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 1647 . . . . . 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 4532 . . . . . . 7  |-  { A }  e.  _V
16 eqeq1 2448 . . . . . . . 8  |-  ( z  =  { A }  ->  ( z  =  { A }  <->  { A }  =  { A } ) )
17 eqeq1 2448 . . . . . . . . . 10  |-  ( z  =  { A }  ->  ( z  =  <. x ,  y >.  <->  { A }  =  <. x ,  y >. ) )
18 eqcom 2444 . . . . . . . . . . 11  |-  ( { A }  =  <. x ,  y >.  <->  <. x ,  y >.  =  { A } )
19 vex 2974 . . . . . . . . . . . 12  |-  x  e. 
_V
20 vex 2974 . . . . . . . . . . . 12  |-  y  e. 
_V
2119, 20, 4opeqsn 4586 . . . . . . . . . . 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 1682 . . . . . . . 8  |-  ( z  =  { A }  ->  ( E. x E. y  z  =  <. x ,  y >.  <->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
2516, 24imbi12d 320 . . . . . . 7  |-  ( z  =  { A }  ->  ( ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  <->  ( { A }  =  { A }  ->  E. x E. y
( x  =  y  /\  A  =  {
x } ) ) ) )
2615, 25spcv 3062 . . . . . 6  |-  ( A. z ( z  =  { A }  ->  E. x E. y  z  =  <. x ,  y
>. )  ->  ( { A }  =  { A }  ->  E. x E. y ( x  =  y  /\  A  =  { x } ) ) )
27 sneq 3886 . . . . . . . . 9  |-  ( w  =  x  ->  { w }  =  { x } )
2827eqeq2d 2453 . . . . . . . 8  |-  ( w  =  x  ->  ( A  =  { w } 
<->  A  =  { x } ) )
2928cbvexv 1972 . . . . . . 7  |-  ( E. w  A  =  {
w }  <->  E. x  A  =  { x } )
30 ax6ev 1710 . . . . . . . . . 10  |-  E. y 
y  =  x
31 equcom 1732 . . . . . . . . . . 11  |-  ( y  =  x  <->  x  =  y )
3231exbii 1634 . . . . . . . . . 10  |-  ( E. y  y  =  x  <->  E. y  x  =  y )
3330, 32mpbi 208 . . . . . . . . 9  |-  E. y  x  =  y
34 19.41v 1920 . . . . . . . . 9  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
( E. y  x  =  y  /\  A  =  { x } ) )
3533, 34mpbiran 909 . . . . . . . 8  |-  ( E. y ( x  =  y  /\  A  =  { x } )  <-> 
A  =  { x } )
3635exbii 1634 . . . . . . 7  |-  ( E. x E. y ( x  =  y  /\  A  =  { x } )  <->  E. x  A  =  { x } )
37 eqid 2442 . . . . . . . 8  |-  { A }  =  { A }
3837a1bi 337 . . . . . . 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 2442 . . . . . 6  |-  { A ,  B }  =  { A ,  B }
42 prex 4533 . . . . . . 7  |-  { A ,  B }  e.  _V
43 eqeq1 2448 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( z  =  { A ,  B }  <->  { A ,  B }  =  { A ,  B } ) )
44 eqeq1 2448 . . . . . . . . 9  |-  ( z  =  { A ,  B }  ->  ( z  =  <. x ,  y
>. 
<->  { A ,  B }  =  <. x ,  y >. ) )
45442exbidv 1682 . . . . . . . 8  |-  ( z  =  { A ,  B }  ->  ( E. x E. y  z  =  <. x ,  y
>. 
<->  E. x E. y { A ,  B }  =  <. x ,  y
>. ) )
4643, 45imbi12d 320 . . . . . . 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 3062 . . . . . 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 2444 . . . . . . . . . 10  |-  ( { A ,  B }  =  <. x ,  y
>. 
<-> 
<. x ,  y >.  =  { A ,  B } )
5019, 20, 4, 5opeqpr 4587 . . . . . . . . . 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 2460 . . . . . . . . . . . . . 14  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  { x ,  y }  =  { w } )
54 vex 2974 . . . . . . . . . . . . . . . 16  |-  w  e. 
_V
5519, 20, 54preqsn 4054 . . . . . . . . . . . . . . 15  |-  ( { x ,  y }  =  { w }  <->  ( x  =  y  /\  y  =  w )
)
5655simplbi 460 . . . . . . . . . . . . . 14  |-  ( { x ,  y }  =  { w }  ->  x  =  y )
5753, 56syl 16 . . . . . . . . . . . . 13  |-  ( ( A  =  { x ,  y }  /\  A  =  { w } )  ->  x  =  y )
58 dfsn2 3889 . . . . . . . . . . . . . . . . . . . 20  |-  { x }  =  { x ,  x }
59 preq2 3954 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  { x ,  x }  =  {
x ,  y } )
6058, 59syl5req 2487 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x ,  y }  =  { x } )
6160eqeq2d 2453 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( A  =  { x ,  y }  <->  A  =  { x } ) )
6258, 59syl5eq 2486 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  { x }  =  { x ,  y } )
6362eqeq2d 2453 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  ( B  =  { x } 
<->  B  =  { x ,  y } ) )
6461, 63anbi12d 710 . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . 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 435 . . . . . . . . . . 11  |-  ( A  =  { w }  ->  ( A  =  {
x ,  y }  ->  ( B  =  { x }  ->  ( A  =  { x }  /\  B  =  {
x ,  y } ) ) ) )
7170impd 431 . . . . . . . . . 10  |-  ( A  =  { w }  ->  ( ( A  =  { x ,  y }  /\  B  =  { x } )  ->  ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7252, 71jaod 380 . . . . . . . . 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 1678 . . . . . . 7  |-  ( A  =  { w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y >.  ->  E. x E. y ( A  =  { x }  /\  B  =  { x ,  y } ) ) )
7574exlimiv 1688 . . . . . 6  |-  ( E. w  A  =  {
w }  ->  ( E. x E. y { A ,  B }  =  <. x ,  y
>.  ->  E. x E. y
( A  =  {
x }  /\  B  =  { x ,  y } ) ) )
7675imp 429 . . . . 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 477 . . . 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 461 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  { A } )
80 equid 1729 . . . . . . . . . . . . . 14  |-  x  =  x
8180jctl 541 . . . . . . . . . . . . 13  |-  ( A  =  { x }  ->  ( x  =  x  /\  A  =  {
x } ) )
8219, 19, 4opeqsn 4586 . . . . . . . . . . . . 13  |-  ( <.
x ,  x >.  =  { A }  <->  ( x  =  x  /\  A  =  { x } ) )
8381, 82sylibr 212 . . . . . . . . . . . 12  |-  ( A  =  { x }  -> 
<. x ,  x >.  =  { A } )
8483adantr 465 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  <. x ,  x >.  =  { A } )
8579, 84eqtr4d 2477 . . . . . . . . . 10  |-  ( ( A  =  { x }  /\  z  =  { A } )  ->  z  =  <. x ,  x >. )
86 opeq12 4060 . . . . . . . . . . . 12  |-  ( ( w  =  x  /\  v  =  x )  -> 
<. w ,  v >.  =  <. x ,  x >. )
8786eqeq2d 2453 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  x )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  x >. ) )
8819, 19, 87spc2ev 3064 . . . . . . . . . 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 714 . . . . . . . 8  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A } )  ->  E. w E. v 
z  =  <. w ,  v >. )
91 preq12 3955 . . . . . . . . . . . 12  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  { A ,  B }  =  { { x } ,  { x ,  y } } )
9291eqeq2d 2453 . . . . . . . . . . 11  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( z  =  { A ,  B } 
<->  z  =  { {
x } ,  {
x ,  y } } ) )
9392biimpa 484 . . . . . . . . . 10  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  { { x } ,  { x ,  y } } )
9419, 20dfop 4057 . . . . . . . . . 10  |-  <. x ,  y >.  =  { { x } ,  { x ,  y } }
9593, 94syl6eqr 2492 . . . . . . . . 9  |-  ( ( ( A  =  {
x }  /\  B  =  { x ,  y } )  /\  z  =  { A ,  B } )  ->  z  =  <. x ,  y
>. )
96 opeq12 4060 . . . . . . . . . . 11  |-  ( ( w  =  x  /\  v  =  y )  -> 
<. w ,  v >.  =  <. x ,  y
>. )
9796eqeq2d 2453 . . . . . . . . . 10  |-  ( ( w  =  x  /\  v  =  y )  ->  ( z  =  <. w ,  v >.  <->  z  =  <. x ,  y >.
) )
9819, 20, 97spc2ev 3064 . . . . . . . . 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 434 . . . . . 6  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  ( (
z  =  { A }  \/  z  =  { A ,  B }
)  ->  E. w E. v  z  =  <. w ,  v >.
) )
102 elvv 4896 . . . . . 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 3361 . . . 4  |-  ( ( A  =  { x }  /\  B  =  {
x ,  y } )  ->  <. A ,  B >.  C_  ( _V  X.  _V ) )
105104exlimivv 1689 . . 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 368    /\ wa 369   A.wal 1367    = wceq 1369   E.wex 1586    e. wcel 1756   _Vcvv 2971    C_ wss 3327   {csn 3876   {cpr 3878   <.cop 3882    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 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pr 4530
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-rab 2723  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-opab 4350  df-xp 4845  df-rel 4846
This theorem is referenced by:  funopg  5449
  Copyright terms: Public domain W3C validator