Theorem brsdom 8955

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 8930	. . 3 ⊢ ≺ = ( ≼ ∖ ≈ )
2	1	eleq2i 2854	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≺ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
3		df-br 5101	. 2 ⊢ (𝐴 ≺ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ )
4		df-br 5101	. . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ )
5		df-br 5101	. . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ )
6	5	notbii 322	. . . 4 ⊢ (¬ 𝐴 ≈ 𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )
7	4, 6	anbi12i 637	. . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
8		eldif 3914	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
9	7, 8	bitr4i 280	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
10	2, 3, 9	3bitr4i 305	1 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399   ∈ wcel 2142   ∖ cdif 3901  ⟨cop 4588   class class class wbr 5100   ≈ cen 8924   ≼ cdom 8925   ≺ csdm 8926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-br 5101  df-sdom 8930

This theorem is referenced by:  sdomdom  8961  sdomnen  8962  0sdomg  9078  sdom0  9081  sdomdomtr  9082  domsdomtr  9084  domtriord  9095  canth2  9102  sdomdomtrfi  9169  domsdomtrfi  9170  php2  9176  nnsdomo  9187  1sdom2  9192  sdom1  9194  1sdom2dom  9198  nnsdomg  9243  card2inf  9503  cardsdomelir  9931  cardsdom2  9946  fidomtri2  9952  cardmin2  9957  alephordi  10030  alephord  10031  isfin4p1  10272  isfin5-2  10348  canthnum  10607  canthwe  10609  canthp1  10612  gchdjuidm  10626  gchxpidm  10627  gchhar  10637  axgroth6  10786  hashsdom  14394  ruc  16275  iscard5  44112