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