ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  opth Unicode version

Theorem opth 4055
Description: The ordered pair theorem. If two ordered pairs are equal, their first elements are equal and their second elements are equal. Exercise 6 of [TakeutiZaring] p. 16. Note that  C and  D are not required to be sets due our specific ordered pair definition. (Contributed by NM, 28-May-1995.)
Hypotheses
Ref Expression
opth1.1  |-  A  e. 
_V
opth1.2  |-  B  e. 
_V
Assertion
Ref Expression
opth  |-  ( <. A ,  B >.  = 
<. C ,  D >.  <->  ( A  =  C  /\  B  =  D )
)

Proof of Theorem opth
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 opth1.1 . . . 4  |-  A  e. 
_V
2 opth1.2 . . . 4  |-  B  e. 
_V
31, 2opth1 4054 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  A  =  C )
41, 2opi1 4050 . . . . . . 7  |-  { A }  e.  <. A ,  B >.
5 id 19 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  D >. )
64, 5syl5eleq 2176 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { A }  e.  <. C ,  D >. )
7 oprcl 3641 . . . . . 6  |-  ( { A }  e.  <. C ,  D >.  ->  ( C  e.  _V  /\  D  e.  _V ) )
86, 7syl 14 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( C  e.  _V  /\  D  e.  _V )
)
98simprd 112 . . . 4  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  D  e.  _V )
103opeq1d 3623 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. A ,  B >.  = 
<. C ,  B >. )
1110, 5eqtr3d 2122 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  B >.  = 
<. C ,  D >. )
128simpld 110 . . . . . . . 8  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  C  e.  _V )
13 dfopg 3615 . . . . . . . 8  |-  ( ( C  e.  _V  /\  B  e.  _V )  -> 
<. C ,  B >.  =  { { C } ,  { C ,  B } } )
1412, 2, 13sylancl 404 . . . . . . 7  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  B >.  =  { { C } ,  { C ,  B } } )
1511, 14eqtr3d 2122 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  D >.  =  { { C } ,  { C ,  B } } )
16 dfopg 3615 . . . . . . 7  |-  ( ( C  e.  _V  /\  D  e.  _V )  -> 
<. C ,  D >.  =  { { C } ,  { C ,  D } } )
178, 16syl 14 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  <. C ,  D >.  =  { { C } ,  { C ,  D } } )
1815, 17eqtr3d 2122 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { { C } ,  { C ,  B } }  =  { { C } ,  { C ,  D } } )
19 prexg 4029 . . . . . . 7  |-  ( ( C  e.  _V  /\  B  e.  _V )  ->  { C ,  B }  e.  _V )
2012, 2, 19sylancl 404 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { C ,  B }  e.  _V )
21 prexg 4029 . . . . . . 7  |-  ( ( C  e.  _V  /\  D  e.  _V )  ->  { C ,  D }  e.  _V )
228, 21syl 14 . . . . . 6  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { C ,  D }  e.  _V )
23 preqr2g 3606 . . . . . 6  |-  ( ( { C ,  B }  e.  _V  /\  { C ,  D }  e.  _V )  ->  ( { { C } ,  { C ,  B } }  =  { { C } ,  { C ,  D } }  ->  { C ,  B }  =  { C ,  D } ) )
2420, 22, 23syl2anc 403 . . . . 5  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( { { C } ,  { C ,  B } }  =  { { C } ,  { C ,  D } }  ->  { C ,  B }  =  { C ,  D }
) )
2518, 24mpd 13 . . . 4  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  { C ,  B }  =  { C ,  D } )
26 preq2 3515 . . . . . . 7  |-  ( x  =  D  ->  { C ,  x }  =  { C ,  D }
)
2726eqeq2d 2099 . . . . . 6  |-  ( x  =  D  ->  ( { C ,  B }  =  { C ,  x } 
<->  { C ,  B }  =  { C ,  D } ) )
28 eqeq2 2097 . . . . . 6  |-  ( x  =  D  ->  ( B  =  x  <->  B  =  D ) )
2927, 28imbi12d 232 . . . . 5  |-  ( x  =  D  ->  (
( { C ,  B }  =  { C ,  x }  ->  B  =  x )  <-> 
( { C ,  B }  =  { C ,  D }  ->  B  =  D ) ) )
30 vex 2622 . . . . . 6  |-  x  e. 
_V
312, 30preqr2 3608 . . . . 5  |-  ( { C ,  B }  =  { C ,  x }  ->  B  =  x )
3229, 31vtoclg 2679 . . . 4  |-  ( D  e.  _V  ->  ( { C ,  B }  =  { C ,  D }  ->  B  =  D ) )
339, 25, 32sylc 61 . . 3  |-  ( <. A ,  B >.  = 
<. C ,  D >.  ->  B  =  D )
343, 33jca 300 . 2  |-  ( <. A ,  B >.  = 
<. C ,  D >.  -> 
( A  =  C  /\  B  =  D ) )
35 opeq12 3619 . 2  |-  ( ( A  =  C  /\  B  =  D )  -> 
<. A ,  B >.  = 
<. C ,  D >. )
3634, 35impbii 124 1  |-  ( <. A ,  B >.  = 
<. C ,  D >.  <->  ( A  =  C  /\  B  =  D )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    = wceq 1289    e. wcel 1438   _Vcvv 2619   {csn 3441   {cpr 3442   <.cop 3444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450
This theorem is referenced by:  opthg  4056  otth2  4059  copsexg  4062  copsex4g  4065  opcom  4068  moop2  4069  opelopabsbALT  4077  opelopabsb  4078  ralxpf  4570  rexxpf  4571  cnvcnvsn  4894  funopg  5034  funinsn  5049  brabvv  5677  xpdom2  6527  xpf1o  6540  djuf1olem  6724  enq0ref  6971  enq0tr  6972  mulnnnq0  6988  eqresr  7352  cnref1o  9102  fisumcom2  10795  qredeu  11172
  Copyright terms: Public domain W3C validator