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

Theorem brsdom 6817
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 6799 . . 3  |-  ~<  =  (  ~<_  \  ~~  )
21eleq2i 2320 . 2  |-  ( <. A ,  B >.  e. 
~< 
<-> 
<. A ,  B >.  e.  (  ~<_  \  ~~  ) )
3 df-br 3964 . 2  |-  ( A 
~<  B  <->  <. A ,  B >.  e.  ~<  )
4 df-br 3964 . . . 4  |-  ( A  ~<_  B  <->  <. A ,  B >.  e.  ~<_  )
5 df-br 3964 . . . . 5  |-  ( A 
~~  B  <->  <. A ,  B >.  e.  ~~  )
65notbii 289 . . . 4  |-  ( -.  A  ~~  B  <->  -.  <. A ,  B >.  e.  ~~  )
74, 6anbi12i 681 . . 3  |-  ( ( A  ~<_  B  /\  -.  A  ~~  B )  <->  ( <. A ,  B >.  e.  ~<_  /\  -.  <. A ,  B >.  e. 
~~  ) )
8 eldif 3104 . . 3  |-  ( <. A ,  B >.  e.  (  ~<_  \  ~~  )  <->  ( <. A ,  B >.  e.  ~<_  /\  -.  <. A ,  B >.  e. 
~~  ) )
97, 8bitr4i 245 . 2  |-  ( ( A  ~<_  B  /\  -.  A  ~~  B )  <->  <. A ,  B >.  e.  (  ~<_  \  ~~  ) )
102, 3, 93bitr4i 270 1  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178    /\ wa 360    e. wcel 1621    \ cdif 3091   <.cop 3584   class class class wbr 3963    ~~ cen 6793    ~<_ cdom 6794    ~< csdm 6795
This theorem is referenced by:  sdomdom  6822  sdomnen  6823  0sdomg  6923  sdomdomtr  6927  domsdomtr  6929  domtriord  6940  canth2  6947  php2  6979  php3  6980  nnsdomo  6988  nnsdomg  7049  card2inf  7202  cardsdomelir  7539  cardsdom2  7554  fidomtri2  7560  cardmin2  7564  alephordi  7634  alephord  7635  isfin4-3  7874  isfin5-2  7950  canthnum  8204  canthwe  8206  canthp1  8209  gchcdaidm  8223  gchxpidm  8224  gchhar  8226  axgroth6  8383  hashsdom  11294  ruc  12448  carinttar  25234
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-dif 3097  df-br 3964  df-sdom 6799
  Copyright terms: Public domain W3C validator