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

Metamath Proof Explorer

Theorem entric

Description: Trichotomy of equinumerosity and strict dominance. This theorem is equivalent to the Axiom of Choice. Theorem 8 of Suppes p. 242. (Contributed by NM, 4-Jan-2004)

		Ref	Expression
	Assertion	entric	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ∨ 𝐵 ≺ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		domtri	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )
2	1	biimprd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝐵 ≺ 𝐴 → 𝐴 ≼ 𝐵 ) )
3		brdom2	⊢ ( 𝐴 ≼ 𝐵 ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) )
4	2 3	imbitrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ 𝐵 ≺ 𝐴 → ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ) )
5	4	con1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ¬ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) → 𝐵 ≺ 𝐴 ) )
6	5	orrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ∨ 𝐵 ≺ 𝐴 ) )
7		df-3or	⊢ ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ∨ 𝐵 ≺ 𝐴 ) ↔ ( ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ∨ 𝐵 ≺ 𝐴 ) )
8	6 7	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ∨ 𝐵 ≺ 𝐴 ) )