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

Theorem brsdom 8251
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 8231 . . 3 ≺ = ( ≼ ∖ ≈ )
21eleq2i 2898 . 2 (⟨𝐴, 𝐵⟩ ∈ ≺ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
3 df-br 4876 . 2 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ )
4 df-br 4876 . . . 4 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ )
5 df-br 4876 . . . . 5 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ )
65notbii 312 . . . 4 𝐴𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )
74, 6anbi12i 620 . . 3 ((𝐴𝐵 ∧ ¬ 𝐴𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
8 eldif 3808 . . 3 (⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
97, 8bitr4i 270 . 2 ((𝐴𝐵 ∧ ¬ 𝐴𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
102, 3, 93bitr4i 295 1 (𝐴𝐵 ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 198  wa 386  wcel 2164  cdif 3795  cop 4405   class class class wbr 4875  cen 8225  cdom 8226  csdm 8227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-dif 3801  df-br 4876  df-sdom 8231
This theorem is referenced by:  sdomdom  8256  sdomnen  8257  0sdomg  8364  sdomdomtr  8368  domsdomtr  8370  domtriord  8381  canth2  8388  php2  8420  php3  8421  nnsdomo  8430  nnsdomg  8494  card2inf  8736  cardsdomelir  9119  cardsdom2  9134  fidomtri2  9140  cardmin2  9144  alephordi  9217  alephord  9218  isfin4-3  9459  isfin5-2  9535  canthnum  9793  canthwe  9795  canthp1  9798  gchcdaidm  9812  gchxpidm  9813  gchhar  9823  axgroth6  9972  hashsdom  13467  ruc  15353
  Copyright terms: Public domain W3C validator