Theorem bren2 8954

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 8950	. . 3 ⊢ (𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵)
2		sdomnen 8952	. . . 4 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵)
3	2	con2i 139	. . 3 ⊢ (𝐴 ≈ 𝐵 → ¬ 𝐴 ≺ 𝐵)
4	1, 3	jca 511	. 2 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵))
5		brdom2 8953	. . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
6	5	biimpi 216	. . 3 ⊢ (𝐴 ≼ 𝐵 → (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
7	6	orcanai 1004	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵) → 𝐴 ≈ 𝐵)
8	4, 7	impbii 209	1 ⊢ (𝐴 ≈ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847   class class class wbr 5107   ≈ cen 8915   ≼ cdom 8916   ≺ csdm 8917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-f1o 6518  df-en 8919  df-dom 8920  df-sdom 8921

This theorem is referenced by:  marypha1lem  9384  tskwe  9903  infxpenlem  9966  cdainflem  10141  axcclem  10410  alephsuc3  10533  gchen1  10578  gchen2  10579  inatsk  10731  ufilen  23817  dirith2  27439  f1ocnt  32725  lindsenlbs  37609  mblfinlem1  37651  axccdom  45216  axccd2  45224