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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		entri2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≺ 𝐴 ) )
2		sdomdom	⊢ ( 𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴 )
3	2	orim2i	⊢ ( ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≺ 𝐴 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )
4	1 3	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≼ 𝐴 ) )