Theorem brsdom 5440

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 5429	. . 3 |- ~< = ( ~<_ \ ~~ )
2	1	eleq2i 1961	. 2 |- (<.A, B>. e. ~< <-> <.A, B>. e. ( ~<_ \ ~~ ))
3		df-br 3339	. 2 |- (A ~< B <-> <.A, B>. e. ~< )
4		df-br 3339	. . . 4 |- (A ~<_ B <-> <.A, B>. e. ~<_ )
5		df-br 3339	. . . . 5 |- (A ~~ B <-> <.A, B>. e. ~~ )
6	5	notbii 204	. . . 4 |- (-. A ~~ B <-> -. <.A, B>. e. ~~ )
7	4, 6	anbi12i 540	. . 3 |- ((A ~<_ B /\ -. A ~~ B) <-> (<.A, B>. e. ~<_ /\ -. <.A, B>. e. ~~ ))
8		eldif 2609	. . 3 |- (<.A, B>. e. ( ~<_ \ ~~ ) <-> (<.A, B>. e. ~<_ /\ -. <.A, B>. e. ~~ ))
9	7, 8	bitr4i 193	. 2 |- ((A ~<_ B /\ -. A ~~ B) <-> <.A, B>. e. ( ~<_ \ ~~ ))
10	2, 3, 9	3bitr4i 200	1 |- (A ~< B <-> (A ~<_ B /\ -. A ~~ B))

Syntax hints:  -. wn 2   <-> wb 163   /\ wa 240   e. wcel 1300   \ cdif 2590  <.cop 3046   class class class wbr 3338   ~~ cen 5423   ~<_ cdom 5424   ~< csdm 5425

This theorem is referenced by:  sdomdom 5445  sdomnen 5446  0sdomg 5529  ensdomtr 5534  domsdomtr 5539  domtriord 5546  canth2 5548  php2 5608  php3 5609  nnsdomo 5615  infsdomnn 5625  unfi2 5645  unifi2 5649  onsdom 5694  isfinite 5741  nnsdom 5742  omsubsdom 5881  elomsubsd 5885  cardsdom 5988  cardsdomel 6004  alephordi 6022  alephord 6023  ruc 8818  axgroth6 10137  isfinite1b 14434  tarax3e 15228  carinttar 15279  dmsdtriordOLD 15360  onsdomOLD 15385  omsubsdomOLD 15390  elomsubsdOLD 15394

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-dif 2597  df-br 3339  df-sdom 5429

Copyright terms: Public domain