Theorem brsdom 8515

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

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   ∈ wcel 2111   ∖ cdif 3878  ⟨cop 4531   class class class wbr 5030   ≈ cen 8489   ≼ cdom 8490   ≺ csdm 8491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-br 5031  df-sdom 8495

This theorem is referenced by:  sdomdom  8520  sdomnen  8521  0sdomg  8630  sdomdomtr  8634  domsdomtr  8636  domtriord  8647  canth2  8654  php2  8686  php3  8687  nnsdomo  8698  nnsdomg  8761  card2inf  9003  cardsdomelir  9386  cardsdom2  9401  fidomtri2  9407  cardmin2  9412  alephordi  9485  alephord  9486  isfin4p1  9726  isfin5-2  9802  canthnum  10060  canthwe  10062  canthp1  10065  gchdjuidm  10079  gchxpidm  10080  gchhar  10090  axgroth6  10239  hashsdom  13738  ruc  15588  iscard5  40242