# Metamath Proof Explorer

## Theorem entri2

Description: Trichotomy of dominance and strict dominance. (Contributed by NM, 4-Jan-2004)

Ref Expression
Assertion entri2 ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}\preccurlyeq {B}\vee {B}\prec {A}\right)$

### Proof

Step Hyp Ref Expression
1 entric ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}\prec {B}\vee {A}\approx {B}\vee {B}\prec {A}\right)$
2 brdom2 ${⊢}{A}\preccurlyeq {B}↔\left({A}\prec {B}\vee {A}\approx {B}\right)$
3 2 orbi1i ${⊢}\left({A}\preccurlyeq {B}\vee {B}\prec {A}\right)↔\left(\left({A}\prec {B}\vee {A}\approx {B}\right)\vee {B}\prec {A}\right)$
4 df-3or ${⊢}\left({A}\prec {B}\vee {A}\approx {B}\vee {B}\prec {A}\right)↔\left(\left({A}\prec {B}\vee {A}\approx {B}\right)\vee {B}\prec {A}\right)$
5 3 4 bitr4i ${⊢}\left({A}\preccurlyeq {B}\vee {B}\prec {A}\right)↔\left({A}\prec {B}\vee {A}\approx {B}\vee {B}\prec {A}\right)$
6 1 5 sylibr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}\preccurlyeq {B}\vee {B}\prec {A}\right)$