Theorem brsdom

Description: Strict dominance relation, meaning " B is strictly greater in size than A ". Definition of Mendelson p. 255. (Contributed by NM, 25-Jun-1998)

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

Proof

Step	Hyp	Ref	Expression
1		df-sdom	|- ~< = ( ~<_ \ ~~ )
2	1	eleq2i	|- ( <. A , B >. e. ~< <-> <. A , B >. e. ( ~<_ \ ~~ ) )
3		df-br	|- ( A ~< B <-> <. A , B >. e. ~< )
4		df-br	|- ( A ~<_ B <-> <. A , B >. e. ~<_ )
5		df-br	|- ( A ~~ B <-> <. A , B >. e. ~~ )
6	5	notbii	|- ( -. A ~~ B <-> -. <. A , B >. e. ~~ )
7	4 6	anbi12i	|- ( ( A ~<_ B /\ -. A ~~ B ) <-> ( <. A , B >. e. ~<_ /\ -. <. A , B >. e. ~~ ) )
8		eldif	|- ( <. A , B >. e. ( ~<_ \ ~~ ) <-> ( <. A , B >. e. ~<_ /\ -. <. A , B >. e. ~~ ) )
9	7 8	bitr4i	|- ( ( A ~<_ B /\ -. A ~~ B ) <-> <. A , B >. e. ( ~<_ \ ~~ ) )
10	2 3 9	3bitr4i	|- ( A ~< B <-> ( A ~<_ B /\ -. A ~~ B ) )