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

Theorem brsdom 9006
Description: Strict dominance relation, meaning "𝐵 is strictly greater in size than 𝐴". Definition of [Mendelson] p. 255. (Contributed by NM, 25-Jun-1998.)
Assertion
Ref Expression
brsdom (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))

Proof of Theorem brsdom
StepHypRef Expression
1 df-sdom 8977 . . 3 ≺ = ( ≼ ∖ ≈ )
21eleq2i 2818 . 2 (⟨𝐴, 𝐵⟩ ∈ ≺ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
3 df-br 5154 . 2 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ )
4 df-br 5154 . . . 4 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ )
5 df-br 5154 . . . . 5 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ )
65notbii 319 . . . 4 𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )
74, 6anbi12i 626 . . 3 ((𝐴𝐵 ∧ ¬ 𝐴𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
8 eldif 3957 . . 3 (⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
97, 8bitr4i 277 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
102, 3, 93bitr4i 302 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 394  wcel 2099  cdif 3944  cop 4639   class class class wbr 5153  cen 8971  cdom 8972  csdm 8973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3950  df-br 5154  df-sdom 8977
This theorem is referenced by:  sdomdom  9011  sdomnen  9012  0sdomg  9142  0sdomgOLD  9143  sdom0  9146  sdomdomtr  9148  domsdomtr  9150  domtriord  9161  canth2  9168  sdomdomtrfi  9238  domsdomtrfi  9239  php2  9245  php2OLD  9257  php3OLD  9258  nnsdomo  9268  1sdom2  9274  sdom1  9276  1sdom2dom  9281  nnsdomg  9336  nnsdomgOLD  9337  card2inf  9598  cardsdomelir  10016  cardsdom2  10031  fidomtri2  10037  cardmin2  10042  alephordi  10117  alephord  10118  isfin4p1  10358  isfin5-2  10434  canthnum  10692  canthwe  10694  canthp1  10697  gchdjuidm  10711  gchxpidm  10712  gchhar  10722  axgroth6  10871  hashsdom  14398  ruc  16245  iscard5  43203
  Copyright terms: Public domain W3C validator