Theorem brsdom 4522

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 4511	. . 3 |- ~< = ( ~<_ \ ~~ )
2	1	eleq2i 1581	. 2 |- (<.A, B>. e. ~< <-> <.A, B>. e. ( ~<_ \ ~~ ))
3		df-br 2693	. 2 |- (A ~< B <-> <.A, B>. e. ~< )
4		df-br 2693	. . . 4 |- (A ~<_ B <-> <.A, B>. e. ~<_ )
5		df-br 2693	. . . . 5 |- (A ~~ B <-> <.A, B>. e. ~~ )
6	5	notbii 185	. . . 4 |- (-. A ~~ B <-> -. <.A, B>. e. ~~ )
7	4, 6	anbi12i 485	. . 3 |- ((A ~<_ B /\ -. A ~~ B) <-> (<.A, B>. e. ~<_ /\ -. <.A, B>. e. ~~ ))
8		eldif 2109	. . 3 |- (<.A, B>. e. ( ~<_ \ ~~ ) <-> (<.A, B>. e. ~<_ /\ -. <.A, B>. e. ~~ ))
9	7, 8	bitr4i 174	. 2 |- ((A ~<_ B /\ -. A ~~ B) <-> <.A, B>. e. ( ~<_ \ ~~ ))
10	2, 3, 9	3bitr4i 181	1 |- (A ~< B <-> (A ~<_ B /\ -. A ~~ B))

Syntax hints:  -. wn 2   <-> wb 144   /\ wa 221   e. wcel 994   \ cdif 2096  <.cop 2469   class class class wbr 2692   ~~ cen 4505   ~<_ cdom 4506   ~< csdm 4507

This theorem is referenced by:  sdomdom 4527  sdomnen 4528  0sdomg 4611  ensdomtr 4616  domsdomtr 4621  canth2 4629  php2 4661  php3 4662  nnsdomo 4668  infsdomnn 4678  unfi2 4698  unifi2 4702  isfinite 4780  nnsdom 4781  cardsdom 4986  cardsdomel 5002  alephordi 5024  alephord 5025  ruc 7761  dmsdtriord 11408  onsdom 11437  omsubsdom 11442  elomsubsd 11446

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-dif 2101  df-br 2693  df-sdom 4511

Copyright terms: Public domain