Theorem bren2

Description: Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004)

	Ref	Expression
Assertion	bren2	$$⊢A\approx B\leftrightarrow \left(A\preccurlyeq B\wedge \neg A\prec B\right)$$

Proof

Step	Hyp	Ref	Expression
1		endom	$$⊢A\approx B\to A\preccurlyeq B$$
2		sdomnen	$$⊢A\prec B\to \neg A\approx B$$
3	2	con2i	$$⊢A\approx B\to \neg A\prec B$$
4	1 3	jca	$$⊢A\approx B\to \left(A\preccurlyeq B\wedge \neg A\prec B\right)$$
5		brdom2	$$⊢A\preccurlyeq B\leftrightarrow \left(A\prec B\vee A\approx B\right)$$
6	5	biimpi	$$⊢A\preccurlyeq B\to \left(A\prec B\vee A\approx B\right)$$
7	6	orcanai	$$⊢\left(A\preccurlyeq B\wedge \neg A\prec B\right)\to A\approx B$$
8	4 7	impbii	$$⊢A\approx B\leftrightarrow \left(A\preccurlyeq B\wedge \neg A\prec B\right)$$