This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem entri3

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 ∈ V ∧ B ∈ W → A ≼ B ∨ B ≼ A

Proof

Step Hyp Ref Expression
1 entri2 ⊢ A ∈ V ∧ B ∈ 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 ∈ V ∧ B ∈ W → A ≼ B ∨ B ≼ A