Theorem brsdom2

Description: Alternate definition of strict dominance. Definition 3 of Suppes p. 97. (Contributed by NM, 27-Jul-2004)

	Ref	Expression
Hypotheses	brsdom2.1	|- A e. _V
	brsdom2.2	|- B e. _V
Assertion	brsdom2	|- ( A ~< B <-> ( A ~<_ B /\ -. B ~<_ A ) )

Proof

Step	Hyp	Ref	Expression
1		brsdom2.1	|- A e. _V
2		brsdom2.2	|- B e. _V
3		dfsdom2	|- ~< = ( ~<_ \ `' ~<_ )
4	3	eleq2i	|- ( <. A , B >. e. ~< <-> <. A , B >. e. ( ~<_ \ `' ~<_ ) )
5		df-br	|- ( A ~< B <-> <. A , B >. e. ~< )
6		df-br	|- ( A ~<_ B <-> <. A , B >. e. ~<_ )
7		df-br	|- ( B ~<_ A <-> <. B , A >. e. ~<_ )
8	1 2	opelcnv	|- ( <. A , B >. e. `' ~<_ <-> <. B , A >. e. ~<_ )
9	7 8	bitr4i	|- ( B ~<_ A <-> <. A , B >. e. `' ~<_ )
10	9	notbii	|- ( -. B ~<_ A <-> -. <. A , B >. e. `' ~<_ )
11	6 10	anbi12i	|- ( ( A ~<_ B /\ -. B ~<_ A ) <-> ( <. A , B >. e. ~<_ /\ -. <. A , B >. e. `' ~<_ ) )
12		eldif	|- ( <. A , B >. e. ( ~<_ \ `' ~<_ ) <-> ( <. A , B >. e. ~<_ /\ -. <. A , B >. e. `' ~<_ ) )
13	11 12	bitr4i	|- ( ( A ~<_ B /\ -. B ~<_ A ) <-> <. A , B >. e. ( ~<_ \ `' ~<_ ) )
14	4 5 13	3bitr4i	|- ( A ~< B <-> ( A ~<_ B /\ -. B ~<_ A ) )