Description: Trichotomy of dominance. This theorem is equivalent to the Axiom of Choice. Part of Proposition 4.42(d) of Mendelson p. 275. (Contributed by NM, 4-Jan-2004)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | entri3 | |- ( ( A e. V /\ B e. W ) -> ( A ~<_ B \/ B ~<_ A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | entri2 | |- ( ( A e. V /\ B e. W ) -> ( A ~<_ B \/ B ~< A ) ) |
|
| 2 | sdomdom | |- ( B ~< A -> B ~<_ A ) |
|
| 3 | 2 | orim2i | |- ( ( A ~<_ B \/ B ~< A ) -> ( A ~<_ B \/ B ~<_ A ) ) |
| 4 | 1 3 | syl | |- ( ( A e. V /\ B e. W ) -> ( A ~<_ B \/ B ~<_ A ) ) |