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

Theorem brsdom 8519
 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 8499 . . 3 ≺ = ( ≼ ∖ ≈ )
21eleq2i 2905 . 2 (⟨𝐴, 𝐵⟩ ∈ ≺ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
3 df-br 5043 . 2 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ )
4 df-br 5043 . . . 4 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ )
5 df-br 5043 . . . . 5 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ )
65notbii 323 . . . 4 𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )
74, 6anbi12i 629 . . 3 ((𝐴𝐵 ∧ ¬ 𝐴𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
8 eldif 3918 . . 3 (⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
97, 8bitr4i 281 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
102, 3, 93bitr4i 306 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∈ wcel 2114   ∖ cdif 3905  ⟨cop 4545   class class class wbr 5042   ≈ cen 8493   ≼ cdom 8494   ≺ csdm 8495 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-dif 3911  df-br 5043  df-sdom 8499 This theorem is referenced by:  sdomdom  8524  sdomnen  8525  0sdomg  8634  sdomdomtr  8638  domsdomtr  8640  domtriord  8651  canth2  8658  php2  8690  php3  8691  nnsdomo  8702  nnsdomg  8765  card2inf  9007  cardsdomelir  9390  cardsdom2  9405  fidomtri2  9411  cardmin2  9416  alephordi  9489  alephord  9490  isfin4p1  9726  isfin5-2  9802  canthnum  10060  canthwe  10062  canthp1  10065  gchdjuidm  10079  gchxpidm  10080  gchhar  10090  axgroth6  10239  hashsdom  13738  ruc  15587  iscard5  40172
 Copyright terms: Public domain W3C validator