Theorem brsdom 7841

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

Step	Hyp	Ref	Expression
1		df-sdom 7821	. . 3 ⊢ ≺ = ( ≼ ∖ ≈ )
2	1	eleq2i 2679	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≺ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
3		df-br 4578	. 2 ⊢ (𝐴 ≺ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ )
4		df-br 4578	. . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ )
5		df-br 4578	. . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ )
6	5	notbii 308	. . . 4 ⊢ (¬ 𝐴 ≈ 𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )
7	4, 6	anbi12i 728	. . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
8		eldif 3549	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
9	7, 8	bitr4i 265	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
10	2, 3, 9	3bitr4i 290	1 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 194   ∧ wa 382   ∈ wcel 1976   ∖ cdif 3536  ⟨cop 4130   class class class wbr 4577   ≈ cen 7815   ≼ cdom 7816   ≺ csdm 7817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-br 4578  df-sdom 7821

This theorem is referenced by:  sdomdom  7846  sdomnen  7847  0sdomg  7951  sdomdomtr  7955  domsdomtr  7957  domtriord  7968  canth2  7975  php2  8007  php3  8008  nnsdomo  8017  nnsdomg  8081  card2inf  8320  cardsdomelir  8659  cardsdom2  8674  fidomtri2  8680  cardmin2  8684  alephordi  8757  alephord  8758  isfin4-3  8997  isfin5-2  9073  canthnum  9327  canthwe  9329  canthp1  9332  gchcdaidm  9346  gchxpidm  9347  gchhar  9357  axgroth6  9506  hashsdom  12983  ruc  14757