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\in \mathrm{V}$$
	brsdom2.2	$$⊢B\in \mathrm{V}$$
Assertion	brsdom2	$$⊢A\prec B\leftrightarrow \left(A\preccurlyeq B\wedge \neg B\preccurlyeq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		brsdom2.1	$$⊢A\in \mathrm{V}$$
2		brsdom2.2	$$⊢B\in \mathrm{V}$$
3		dfsdom2	$$⊢\prec =\preccurlyeq \setminus {\preccurlyeq }^{-1}$$
4	3	eleq2i	$$⊢⟨A,B⟩\in \prec \leftrightarrow ⟨A,B⟩\in \left(\preccurlyeq \setminus {\preccurlyeq }^{-1}\right)$$
5		df-br	$$⊢A\prec B\leftrightarrow ⟨A,B⟩\in \prec$$
6		df-br	$$⊢A\preccurlyeq B\leftrightarrow ⟨A,B⟩\in \preccurlyeq$$
7		df-br	$$⊢B\preccurlyeq A\leftrightarrow ⟨B,A⟩\in \preccurlyeq$$
8	1 2	opelcnv	$$⊢⟨A,B⟩\in {\preccurlyeq }^{-1}\leftrightarrow ⟨B,A⟩\in \preccurlyeq$$
9	7 8	bitr4i	$$⊢B\preccurlyeq A\leftrightarrow ⟨A,B⟩\in {\preccurlyeq }^{-1}$$
10	9	notbii	$$⊢\neg B\preccurlyeq A\leftrightarrow \neg ⟨A,B⟩\in {\preccurlyeq }^{-1}$$
11	6 10	anbi12i	$$⊢\left(A\preccurlyeq B\wedge \neg B\preccurlyeq A\right)\leftrightarrow \left(⟨A,B⟩\in \preccurlyeq \wedge \neg ⟨A,B⟩\in {\preccurlyeq }^{-1}\right)$$
12		eldif	$$⊢⟨A,B⟩\in \left(\preccurlyeq \setminus {\preccurlyeq }^{-1}\right)\leftrightarrow \left(⟨A,B⟩\in \preccurlyeq \wedge \neg ⟨A,B⟩\in {\preccurlyeq }^{-1}\right)$$
13	11 12	bitr4i	$$⊢\left(A\preccurlyeq B\wedge \neg B\preccurlyeq A\right)\leftrightarrow ⟨A,B⟩\in \left(\preccurlyeq \setminus {\preccurlyeq }^{-1}\right)$$
14	4 5 13	3bitr4i	$$⊢A\prec B\leftrightarrow \left(A\preccurlyeq B\wedge \neg B\preccurlyeq A\right)$$