Theorem brsdom 4387

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 4376	. . 3 |- ~< = ( ~<_ \ ~~ )
2	1	eleq2i 1541	. 2 |- (<.A, B>. e. ~< <-> <.A, B>. e. ( ~<_ \ ~~ ))
3		df-br 2625	. 2 |- (A ~< B <-> <.A, B>. e. ~< )
4		df-br 2625	. . . 4 |- (A ~<_ B <-> <.A, B>. e. ~<_ )
5		df-br 2625	. . . . 5 |- (A ~~ B <-> <.A, B>. e. ~~ )
6	5	negbii 187	. . . 4 |- (-. A ~~ B <-> -. <.A, B>. e. ~~ )
7	4, 6	anbi12i 484	. . 3 |- ((A ~<_ B /\ -. A ~~ B) <-> (<.A, B>. e. ~<_ /\ -. <.A, B>. e. ~~ ))
8		eldif 2060	. . 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 960   \ cdif 2047  <.cop 2415   class class class wbr 2624   ~~ cen 4370   ~<_ cdom 4371   ~< csdm 4372

This theorem is referenced by:  sdomdom 4392  sdomnen 4393  0sdomg 4472  ensdomtr 4477  domsdomtr 4482  canth2 4490  php2 4520  php3 4521  php3OLD 4522  nnsdomo 4527  infsdomnn 4541  unfi2 4565  unfi2OLD 4566  unifi2OLD 4571  isfinite 4643  isfiniteOLD 4644  nnsdom 4645  cardsdom 4847  cardsdomel 4863  alephordi 4885  alephord 4886  ruc 7550

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-dif 2052  df-br 2625  df-sdom 4376

Copyright terms: Public domain