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

Theorem brsdom 6884
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 6866 . . 3  |-  ~<  =  (  ~<_  \  ~~  )
21eleq2i 2347 . 2  |-  ( <. A ,  B >.  e. 
~< 
<-> 
<. A ,  B >.  e.  (  ~<_  \  ~~  ) )
3 df-br 4024 . 2  |-  ( A 
~<  B  <->  <. A ,  B >.  e.  ~<  )
4 df-br 4024 . . . 4  |-  ( A  ~<_  B  <->  <. A ,  B >.  e.  ~<_  )
5 df-br 4024 . . . . 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 3162 . . 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 1684    \ cdif 3149   <.cop 3643   class class class wbr 4023    ~~ cen 6860    ~<_ cdom 6861    ~< csdm 6862
This theorem is referenced by:  sdomdom  6889  sdomnen  6890  0sdomg  6990  sdomdomtr  6994  domsdomtr  6996  domtriord  7007  canth2  7014  php2  7046  php3  7047  nnsdomo  7055  nnsdomg  7116  card2inf  7269  cardsdomelir  7606  cardsdom2  7621  fidomtri2  7627  cardmin2  7631  alephordi  7701  alephord  7702  isfin4-3  7941  isfin5-2  8017  canthnum  8271  canthwe  8273  canthp1  8276  gchcdaidm  8290  gchxpidm  8291  gchhar  8293  axgroth6  8450  hashsdom  11363  ruc  12521  carinttar  25902
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 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
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 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-br 4024  df-sdom 6866
  Copyright terms: Public domain W3C validator