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

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 ∨ 𝑋 < 𝑌 ∨ 𝑌 < 𝑋 ) )