Theorem brsdom 4369

Description: Strict dominance relation, meaning "B is strictly greater in size than A." Definition of [Mendelson] p. 255.

Assertion

Ref	Expression
brsdom	|- (A ~< B <-> (A ~<_ B /\ -. A ~~ B))

Proof of Theorem brsdom

Step	Hyp	Ref	Expression
1		df-sdom 4359	. . 3 |- ~< = ( ~<_ \ ~~ )
2	1	eleq2i 1535	. 2 |- (<.A, B>. e. ~< <-> <.A, B>. e. ( ~<_ \ ~~ ))
3		df-br 2615	. 2 |- (A ~< B <-> <.A, B>. e. ~< )
4		df-br 2615	. . . 4 |- (A ~<_ B <-> <.A, B>. e. ~<_ )
5		df-br 2615	. . . . 5 |- (A ~~ B <-> <.A, B>. e. ~~ )
6	5	negbii 187	. . . 4 |- (-. A ~~ B <-> -. <.A, B>. e. ~~ )
7	4, 6	anbi12i 482	. . 3 |- ((A ~<_ B /\ -. A ~~ B) <-> (<.A, B>. e. ~<_ /\ -. <.A, B>. e. ~~ ))
8		eldif 2053	. . 3 |- (<.A, B>. e. ( ~<_ \ ~~ ) <-> (<.A, B>. e. ~<_ /\ -. <.A, B>. e. ~~ ))
9	7, 8	bitr4 176	. 2 |- ((A ~<_ B /\ -. A ~~ B) <-> <.A, B>. e. ( ~<_ \ ~~ ))
10	2, 3, 9	3bitr4 183	1 |- (A ~< B <-> (A ~<_ B /\ -. A ~~ B))

Syntax hints:  -. wn 2   <-> wb 146   /\ wa 223   e. wcel 956   \ cdif 2040  <.cop 2407   class class class wbr 2614   ~~ cen 4354   ~<_ cdom 4355   ~< csdm 4356

This theorem is referenced by:  sdomdom 4373  sdomnen 4374  0sdomg 4452  ensdomtr 4457  domsdomtr 4462  canth2 4470  php2 4500  php3 4501  nnsdomo 4507  infsdomnn 4517  unfi2 4535  unifi2 4539  isfinite 4614  nnsdom 4615  cardsdom 4817  cardsdomel 4832  alephordi 4854  alephord 4855  ruc 7500

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-dif 2045  df-br 2615  df-sdom 4359

Copyright terms: Public domain