Theorem brsdom 8251

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 8231	. . 3 ⊢ ≺ = ( ≼ ∖ ≈ )
2	1	eleq2i 2898	. 2 ⊢ (⟨𝐴, 𝐵⟩ ∈ ≺ ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
3		df-br 4876	. 2 ⊢ (𝐴 ≺ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≺ )
4		df-br 4876	. . . 4 ⊢ (𝐴 ≼ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≼ )
5		df-br 4876	. . . . 5 ⊢ (𝐴 ≈ 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ ≈ )
6	5	notbii 312	. . . 4 ⊢ (¬ 𝐴 ≈ 𝐵 ↔ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ )
7	4, 6	anbi12i 620	. . 3 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
8		eldif 3808	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ) ↔ (⟨𝐴, 𝐵⟩ ∈ ≼ ∧ ¬ ⟨𝐴, 𝐵⟩ ∈ ≈ ))
9	7, 8	bitr4i 270	. 2 ⊢ ((𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵) ↔ ⟨𝐴, 𝐵⟩ ∈ ( ≼ ∖ ≈ ))
10	2, 3, 9	3bitr4i 295	1 ⊢ (𝐴 ≺ 𝐵 ↔ (𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵))

Syntax hints:  ¬ wn 3   ↔ wb 198   ∧ wa 386   ∈ wcel 2164   ∖ cdif 3795  ⟨cop 4405   class class class wbr 4875   ≈ cen 8225   ≼ cdom 8226   ≺ csdm 8227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-dif 3801  df-br 4876  df-sdom 8231

This theorem is referenced by:  sdomdom  8256  sdomnen  8257  0sdomg  8364  sdomdomtr  8368  domsdomtr  8370  domtriord  8381  canth2  8388  php2  8420  php3  8421  nnsdomo  8430  nnsdomg  8494  card2inf  8736  cardsdomelir  9119  cardsdom2  9134  fidomtri2  9140  cardmin2  9144  alephordi  9217  alephord  9218  isfin4-3  9459  isfin5-2  9535  canthnum  9793  canthwe  9795  canthp1  9798  gchcdaidm  9812  gchxpidm  9813  gchhar  9823  axgroth6  9972  hashsdom  13467  ruc  15353