Theorem bren2 8981

Description: Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004.)

Assertion

Ref	Expression
bren2	⊢ (𝐴 ≈ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵))

Proof of Theorem bren2

Step	Hyp	Ref	Expression
1		endom 8977	. . 3 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)
2		sdomnen 8979	. . . 4 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)
3	2	con2i 140	. . 3 ⊢ (𝐴 ≈ 𝐵 → ¬ 𝐴 ≺ 𝐵)
4	1, 3	jca 520	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵))
5		brdom2 8980	. . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
6	5	biimpi 219	. . 3 ⊢ (𝐴 ≼ 𝐵 → (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
7	6	orcanai 1018	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵) → 𝐴 ≈ 𝐵)
8	4, 7	impbii 212	1 ⊢ (𝐴 ≈ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   ∨ wo 860   class class class wbr 5110   ≈ cen 8941   ≼ cdom 8942   ≺ csdm 8943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-br 5111  df-opab 5175  df-f1o 6545  df-en 8945  df-dom 8946  df-sdom 8947

This theorem is referenced by:  marypha1lem  9394  tskwe  9937  infxpenlem  9998  cdainflem  10172  axcclem  10442  alephsuc3  10566  gchen1  10611  gchen2  10612  inatsk  10764  ufilen  24068  dirith2  27673  f1ocnt  33126  kardexen  35557  lindsenlbs  38247  mblfinlem1  38289  axccdom  45921  axccd2  45928