Metamath Proof Explorer


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