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

Theorem brsdom 7089
Description: Strict dominance relation, meaning " B is strictly greater in size than  A." Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.)
Assertion
Ref Expression
brsdom  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )

Proof of Theorem brsdom
StepHypRef Expression
1 df-sdom 7071 . . 3  |-  ~<  =  (  ~<_  \  ~~  )
21eleq2i 2468 . 2  |-  ( <. A ,  B >.  e. 
~< 
<-> 
<. A ,  B >.  e.  (  ~<_  \  ~~  ) )
3 df-br 4173 . 2  |-  ( A 
~<  B  <->  <. A ,  B >.  e.  ~<  )
4 df-br 4173 . . . 4  |-  ( A  ~<_  B  <->  <. A ,  B >.  e.  ~<_  )
5 df-br 4173 . . . . 5  |-  ( A 
~~  B  <->  <. A ,  B >.  e.  ~~  )
65notbii 288 . . . 4  |-  ( -.  A  ~~  B  <->  -.  <. A ,  B >.  e.  ~~  )
74, 6anbi12i 679 . . 3  |-  ( ( A  ~<_  B  /\  -.  A  ~~  B )  <->  ( <. A ,  B >.  e.  ~<_  /\  -.  <. A ,  B >.  e. 
~~  ) )
8 eldif 3290 . . 3  |-  ( <. A ,  B >.  e.  (  ~<_  \  ~~  )  <->  ( <. A ,  B >.  e.  ~<_  /\  -.  <. A ,  B >.  e. 
~~  ) )
97, 8bitr4i 244 . 2  |-  ( ( A  ~<_  B  /\  -.  A  ~~  B )  <->  <. A ,  B >.  e.  (  ~<_  \  ~~  ) )
102, 3, 93bitr4i 269 1  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    /\ wa 359    e. wcel 1721    \ cdif 3277   <.cop 3777   class class class wbr 4172    ~~ cen 7065    ~<_ cdom 7066    ~< csdm 7067
This theorem is referenced by:  sdomdom  7094  sdomnen  7095  0sdomg  7195  sdomdomtr  7199  domsdomtr  7201  domtriord  7212  canth2  7219  php2  7251  php3  7252  nnsdomo  7260  nnsdomg  7325  card2inf  7479  cardsdomelir  7816  cardsdom2  7831  fidomtri2  7837  cardmin2  7841  alephordi  7911  alephord  7912  isfin4-3  8151  isfin5-2  8227  canthnum  8480  canthwe  8482  canthp1  8485  gchcdaidm  8499  gchxpidm  8500  gchhar  8502  axgroth6  8659  hashsdom  11610  ruc  12797
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-br 4173  df-sdom 7071
  Copyright terms: Public domain W3C validator