Theorem brsdom 4363

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 4353	. . 3 |- ~< = ( ~<_ \ ~~ )
2	1	eleq2i 1530	. 2 |- (<.A, B>. e. ~< <-> <.A, B>. e. ( ~<_ \ ~~ ))
3		df-br 2610	. 2 |- (A ~< B <-> <.A, B>. e. ~< )
4		df-br 2610	. . . 4 |- (A ~<_ B <-> <.A, B>. e. ~<_ )
5		df-br 2610	. . . . 5 |- (A ~~ B <-> <.A, B>. e. ~~ )
6	5	negbii 187	. . . 4 |- (-. A ~~ B <-> -. <.A, B>. e. ~~ )
7	4, 6	anbi12i 481	. . 3 |- ((A ~<_ B /\ -. A ~~ B) <-> (<.A, B>. e. ~<_ /\ -. <.A, B>. e. ~~ ))
8		eldif 2047	. . 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 955   \ cdif 2034  <.cop 2401   class class class wbr 2609   ~~ cen 4348   ~<_ cdom 4349   ~< csdm 4350

This theorem is referenced by:  sdomdom 4367  sdomnen 4368  0sdomg 4446  ensdomtr 4451  domsdomtr 4456  canth2 4464  php2 4494  php3 4495  nnsdomo 4501  infsdomnn 4511  unfi2 4529  unifi2 4533  isfinite 4606  nnsdom 4607  cardsdom 4809  cardsdomel 4824  alephordi 4846  alephord 4847  ruc 7492

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-dif 2039  df-br 2610  df-sdom 4353

Copyright terms: Public domain