Theorem tlt3

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

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

Proof

Step	Hyp	Ref	Expression
1		tlt3.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		tlt3.l	⊢ < = ( lt ‘ 𝐾 )
3		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4	1 3 2	tlt2	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∨ 𝑌 < 𝑋 ) )
5		tospos	⊢ ( 𝐾 ∈ Toset → 𝐾 ∈ Poset )
6	1 3 2	pleval2	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) ) )
7		orcom	⊢ ( ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) ↔ ( 𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ) )
8	6 7	bitrdi	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ) ) )
9	5 8	syl3an1	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ↔ ( 𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ) ) )
10	9	orbi1d	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∨ 𝑌 < 𝑋 ) ↔ ( ( 𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ) ∨ 𝑌 < 𝑋 ) ) )
11	4 10	mpbid	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ) ∨ 𝑌 < 𝑋 ) )
12		df-3or	⊢ ( ( 𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋 ) ↔ ( ( 𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ) ∨ 𝑌 < 𝑋 ) )
13	11 12	sylibr	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋 ) )