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

Theorem brsdom 8912
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 8883 . . 3 ≺ = ( ≼ ∖ ≈ )
21eleq2i 2829 . 2 (⟨𝐴, 𝐵⟩ ∈ ≺ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
3 df-br 5105 . 2 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ )
4 df-br 5105 . . . 4 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ )
5 df-br 5105 . . . . 5 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ )
65notbii 319 . . . 4 𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )
74, 6anbi12i 627 . . 3 ((𝐴𝐵 ∧ ¬ 𝐴𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
8 eldif 3919 . . 3 (⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
97, 8bitr4i 277 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
102, 3, 93bitr4i 302 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 396  wcel 2106  cdif 3906  cop 4591   class class class wbr 5104  cen 8877  cdom 8878  csdm 8879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3446  df-dif 3912  df-br 5105  df-sdom 8883
This theorem is referenced by:  sdomdom  8917  sdomnen  8918  0sdomg  9045  0sdomgOLD  9046  sdom0  9049  sdomdomtr  9051  domsdomtr  9053  domtriord  9064  canth2  9071  sdomdomtrfi  9145  domsdomtrfi  9146  php2  9152  php2OLD  9164  php3OLD  9165  nnsdomo  9175  1sdom2  9181  sdom1  9183  1sdom2dom  9188  nnsdomg  9243  nnsdomgOLD  9244  card2inf  9488  cardsdomelir  9906  cardsdom2  9921  fidomtri2  9927  cardmin2  9932  alephordi  10007  alephord  10008  isfin4p1  10248  isfin5-2  10324  canthnum  10582  canthwe  10584  canthp1  10587  gchdjuidm  10601  gchxpidm  10602  gchhar  10612  axgroth6  10761  hashsdom  14278  ruc  16122  iscard5  41788
  Copyright terms: Public domain W3C validator