Theorem tleile

Description: In a Toset, any two elements are comparable. (Contributed by Thierry Arnoux, 11-Feb-2018)

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

Proof

Step	Hyp	Ref	Expression
1		tleile.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		tleile.l	⊢ ≤ = ( le ‘ 𝐾 )
3		simp2	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
4		simp3	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
5	1 2	istos	⊢ ( 𝐾 ∈ Toset ↔ ( 𝐾 ∈ Poset ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) )
6	5	simprbi	⊢ ( 𝐾 ∈ Toset → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
7	6	3ad2ant1	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
8		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦 ) )
9		breq2	⊢ ( 𝑥 = 𝑋 → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ≤ 𝑋 ) )
10	8 9	orbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ↔ ( 𝑋 ≤ 𝑦 ∨ 𝑦 ≤ 𝑋 ) ) )
11		breq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 ≤ 𝑦 ↔ 𝑋 ≤ 𝑌 ) )
12		breq1	⊢ ( 𝑦 = 𝑌 → ( 𝑦 ≤ 𝑋 ↔ 𝑌 ≤ 𝑋 ) )
13	11 12	orbi12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 ≤ 𝑦 ∨ 𝑦 ≤ 𝑋 ) ↔ ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) ) )
14	10 13	rspc2va	⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) → ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) )
15	3 4 7 14	syl21anc	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) )