Theorem entri2

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

	Ref	Expression
Assertion	entri2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≺ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		entric	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ∨ 𝐵 ≺ 𝐴 ) )
2		brdom2	⊢ ( 𝐴 ≼ 𝐵 ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) )
3	2	orbi1i	⊢ ( ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≺ 𝐴 ) ↔ ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ∨ 𝐵 ≺ 𝐴 ) )
4		df-3or	⊢ ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ∨ 𝐵 ≺ 𝐴 ) ↔ ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ∨ 𝐵 ≺ 𝐴 ) )
5	3 4	bitr4i	⊢ ( ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≺ 𝐴 ) ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ∨ 𝐵 ≺ 𝐴 ) )
6	1 5	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≼ 𝐵 ∨ 𝐵 ≺ 𝐴 ) )