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

Theorem dfcnqs 7774
Description: Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in  CC from those in  R.. The trick involves qsid 6558, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that  CC is a quotient set, even though it is not (compare df-c 7751), and allows us to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.)
Assertion
Ref Expression
dfcnqs  |-  CC  =  ( ( R.  X.  R. ) /. `'  _E  )

Proof of Theorem dfcnqs
StepHypRef Expression
1 df-c 7751 . 2  |-  CC  =  ( R.  X.  R. )
2 qsid 6558 . 2  |-  ( ( R.  X.  R. ) /. `'  _E  )  =  ( R.  X.  R. )
31, 2eqtr4i 2188 1  |-  CC  =  ( ( R.  X.  R. ) /. `'  _E  )
Colors of variables: wff set class
Syntax hints:    = wceq 1342    _E cep 4260    X. cxp 4597   `'ccnv 4598   /.cqs 6492   R.cnr 7230   CCcc 7743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-14 2138  ax-ext 2146  ax-sep 4095  ax-pow 4148  ax-pr 4182
This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2724  df-sbc 2948  df-un 3116  df-in 3118  df-ss 3125  df-pw 3556  df-sn 3577  df-pr 3578  df-op 3580  df-br 3978  df-opab 4039  df-eprel 4262  df-xp 4605  df-cnv 4607  df-dm 4609  df-rn 4610  df-res 4611  df-ima 4612  df-ec 6495  df-qs 6499  df-c 7751
This theorem is referenced by:  axmulcom  7804  axaddass  7805  axmulass  7806  axdistr  7807
  Copyright terms: Public domain W3C validator