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

Theorem brsdom 6770
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 6752 . . 3  |-  ~<  =  (  ~<_  \  ~~  )
21eleq2i 2317 . 2  |-  ( <. A ,  B >.  e. 
~< 
<-> 
<. A ,  B >.  e.  (  ~<_  \  ~~  ) )
3 df-br 3921 . 2  |-  ( A 
~<  B  <->  <. A ,  B >.  e.  ~<  )
4 df-br 3921 . . . 4  |-  ( A  ~<_  B  <->  <. A ,  B >.  e.  ~<_  )
5 df-br 3921 . . . . 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 3088 . . 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 3075   <.cop 3547   class class class wbr 3920    ~~ cen 6746    ~<_ cdom 6747    ~< csdm 6748
This theorem is referenced by:  sdomdom  6775  sdomnen  6776  0sdomg  6875  sdomdomtr  6879  domsdomtr  6881  domtriord  6892  canth2  6899  php2  6931  php3  6932  nnsdomo  6940  nnsdomg  7001  card2inf  7153  cardsdomelir  7490  cardsdom2  7505  fidomtri2  7511  cardmin2  7515  alephordi  7585  alephord  7586  isfin4-3  7825  isfin5-2  7901  canthnum  8151  canthwe  8153  canthp1  8156  gchcdaidm  8170  gchxpidm  8171  gchhar  8173  axgroth6  8330  hashsdom  11241  ruc  12395  carinttar  25068
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-dif 3081  df-br 3921  df-sdom 6752
  Copyright terms: Public domain W3C validator