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

Theorem brsdom 6880
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 6862 . . 3  |-  ~<  =  (  ~<_  \  ~~  )
21eleq2i 2348 . 2  |-  ( <. A ,  B >.  e. 
~< 
<-> 
<. A ,  B >.  e.  (  ~<_  \  ~~  ) )
3 df-br 4025 . 2  |-  ( A 
~<  B  <->  <. A ,  B >.  e.  ~<  )
4 df-br 4025 . . . 4  |-  ( A  ~<_  B  <->  <. A ,  B >.  e.  ~<_  )
5 df-br 4025 . . . . 5  |-  ( A 
~~  B  <->  <. A ,  B >.  e.  ~~  )
65notbii 287 . . . 4  |-  ( -.  A  ~~  B  <->  -.  <. A ,  B >.  e.  ~~  )
74, 6anbi12i 678 . . 3  |-  ( ( A  ~<_  B  /\  -.  A  ~~  B )  <->  ( <. A ,  B >.  e.  ~<_  /\  -.  <. A ,  B >.  e. 
~~  ) )
8 eldif 3163 . . 3  |-  ( <. A ,  B >.  e.  (  ~<_  \  ~~  )  <->  ( <. A ,  B >.  e.  ~<_  /\  -.  <. A ,  B >.  e. 
~~  ) )
97, 8bitr4i 243 . 2  |-  ( ( A  ~<_  B  /\  -.  A  ~~  B )  <->  <. A ,  B >.  e.  (  ~<_  \  ~~  ) )
102, 3, 93bitr4i 268 1  |-  ( A 
~<  B  <->  ( A  ~<_  B  /\  -.  A  ~~  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    /\ wa 358    e. wcel 1685    \ cdif 3150   <.cop 3644   class class class wbr 4024    ~~ cen 6856    ~<_ cdom 6857    ~< csdm 6858
This theorem is referenced by:  sdomdom  6885  sdomnen  6886  0sdomg  6986  sdomdomtr  6990  domsdomtr  6992  domtriord  7003  canth2  7010  php2  7042  php3  7043  nnsdomo  7051  nnsdomg  7112  card2inf  7265  cardsdomelir  7602  cardsdom2  7617  fidomtri2  7623  cardmin2  7627  alephordi  7697  alephord  7698  isfin4-3  7937  isfin5-2  8013  canthnum  8267  canthwe  8269  canthp1  8272  gchcdaidm  8286  gchxpidm  8287  gchhar  8289  axgroth6  8446  hashsdom  11359  ruc  12517  carinttar  25313
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-dif 3156  df-br 4025  df-sdom 6862
  Copyright terms: Public domain W3C validator