Description: Trichotomy law for dominance and strict dominance. This theorem is equivalent to the Axiom of Choice. (Contributed by NM, 4-Jan-2004) (Revised by Mario Carneiro, 30-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | domtri | |- ( ( A e. V /\ B e. W ) -> ( A ~<_ B <-> -. B ~< A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | numth3 | |- ( A e. V -> A e. dom card ) |
|
2 | numth3 | |- ( B e. W -> B e. dom card ) |
|
3 | domtri2 | |- ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B <-> -. B ~< A ) ) |
|
4 | 1 2 3 | syl2an | |- ( ( A e. V /\ B e. W ) -> ( A ~<_ B <-> -. B ~< A ) ) |