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

Theorem brdom2 8531
Description: Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97. (Contributed by NM, 17-Jun-1998.)
Assertion
Ref Expression
brdom2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))

Proof of Theorem brdom2
StepHypRef Expression
1 dfdom2 8527 . . 3 ≼ = ( ≺ ∪ ≈ )
21eleq2i 2902 . 2 (⟨𝐴, 𝐵⟩ ∈ ≼ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≺ ∪ ≈ ))
3 df-br 5058 . 2 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ )
4 df-br 5058 . . . 4 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ )
5 df-br 5058 . . . 4 (𝐴𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ )
64, 5orbi12i 910 . . 3 ((𝐴𝐵𝐴𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≺ ∨ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
7 elun 4123 . . 3 (⟨𝐴, 𝐵⟩ ∈ ( ≺ ∪ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≺ ∨ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
86, 7bitr4i 280 . 2 ((𝐴𝐵𝐴𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≺ ∪ ≈ ))
92, 3, 83bitr4i 305 1 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wo 843  wcel 2107  cun 3932  cop 4565   class class class wbr 5057  cen 8498  cdom 8499  csdm 8500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-xp 5554  df-rel 5555  df-f1o 6355  df-en 8502  df-dom 8503  df-sdom 8504
This theorem is referenced by:  bren2  8532  domnsym  8635  modom  8711  carddom2  9398  axcc4dom  9855  entric  9971  entri2  9972  gchor  10041  frgpcyg  20712  iunmbl2  24150  dyadmbl  24193  padct  30447  volmeas  31478  ovoliunnfl  34921  ctbnfien  39400
  Copyright terms: Public domain W3C validator