Theorem brdom2

Description: Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of Suppes p. 97. (Contributed by NM, 17-Jun-1998)

	Ref	Expression
Assertion	brdom2	$$⊢A\preccurlyeq B\leftrightarrow \left(A\prec B\vee A\approx B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfdom2	$$⊢\preccurlyeq =\prec \cup \approx$$
2	1	eleq2i	$$⊢⟨A,B⟩\in \preccurlyeq \leftrightarrow ⟨A,B⟩\in \left(\prec \cup \approx \right)$$
3		df-br	$$⊢A\preccurlyeq B\leftrightarrow ⟨A,B⟩\in \preccurlyeq$$
4		df-br	$$⊢A\prec B\leftrightarrow ⟨A,B⟩\in \prec$$
5		df-br	$$⊢A\approx B\leftrightarrow ⟨A,B⟩\in \approx$$
6	4 5	orbi12i	$$⊢\left(A\prec B\vee A\approx B\right)\leftrightarrow \left(⟨A,B⟩\in \prec \vee ⟨A,B⟩\in \approx \right)$$
7		elun	$$⊢⟨A,B⟩\in \left(\prec \cup \approx \right)\leftrightarrow \left(⟨A,B⟩\in \prec \vee ⟨A,B⟩\in \approx \right)$$
8	6 7	bitr4i	$$⊢\left(A\prec B\vee A\approx B\right)\leftrightarrow ⟨A,B⟩\in \left(\prec \cup \approx \right)$$
9	2 3 8	3bitr4i	$$⊢A\preccurlyeq B\leftrightarrow \left(A\prec B\vee A\approx B\right)$$