Theorem brsdom 8967

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 8942	. . 3 ⊢ ≺ = ( ≼ ∖ ≈ )
2	1	eleq2i 2855	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≺ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
3		df-br 5110	. 2 ⊢ (𝐴 ≺ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ )
4		df-br 5110	. . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ )
5		df-br 5110	. . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ )
6	5	notbii 323	. . . 4 ⊢ (¬ 𝐴 ≈ 𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )
7	4, 6	anbi12i 639	. . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
8		eldif 3915	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
9	7, 8	bitr4i 281	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
10	2, 3, 9	3bitr4i 306	1 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   ∈ wcel 2143   ∖ cdif 3902  ⟨cop 4595   class class class wbr 5109   ≈ cen 8936   ≼ cdom 8937   ≺ csdm 8938

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-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-br 5110  df-sdom 8942

This theorem is referenced by:  sdomdom  8973  sdomnen  8974  0sdomg  9090  sdom0  9093  sdomdomtr  9094  domsdomtr  9096  domtriord  9107  canth2  9114  sdomdomtrfi  9181  domsdomtrfi  9182  php2  9188  nnsdomo  9199  1sdom2  9204  sdom1  9206  1sdom2dom  9210  nnsdomg  9255  card2inf  9513  cardsdomelir  9955  cardsdom2  9970  fidomtri2  9976  cardmin2  9981  alephordi  10054  alephord  10055  isfin4p1  10294  isfin5-2  10370  canthnum  10629  canthwe  10631  canthp1  10634  gchdjuidm  10648  gchxpidm  10649  gchhar  10659  axgroth6  10808  hashsdom  14413  ruc  16294  iscard5  44282