Theorem tlt2

Description: In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 13-Apr-2018)

	Ref	Expression
Hypotheses	tlt2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	tlt2.e	⊢ ≤ = ( le ‘ 𝐾 )
	tlt2.l	⊢ < = ( lt ‘ 𝐾 )
Assertion	tlt2	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		tlt2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		tlt2.e	⊢ ≤ = ( le ‘ 𝐾 )
3		tlt2.l	⊢ < = ( lt ‘ 𝐾 )
4		exmidd	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ∨ ¬ 𝑋 ≤ 𝑌 ) )
5	1 2 3	tltnle	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 < 𝑋 ↔ ¬ 𝑋 ≤ 𝑌 ) )
6	5	3com23	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 < 𝑋 ↔ ¬ 𝑋 ≤ 𝑌 ) )
7	6	orbi2d	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋 ) ↔ ( 𝑋 ≤ 𝑌 ∨ ¬ 𝑋 ≤ 𝑌 ) ) )
8	4 7	mpbird	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ∨ 𝑌 < 𝑋 ) )