Theorem trleile

Description: In a Toset, two elements must compare. (Contributed by Thierry Arnoux, 12-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		trleile.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		trleile.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4	1 3	tleile	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∨ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) )
5		3simpc	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
6		brxp	⊢ ( 𝑋 ( 𝐵 × 𝐵 ) 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
7	5 6	sylibr	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( 𝐵 × 𝐵 ) 𝑌 )
8		brin	⊢ ( 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑋 ( 𝐵 × 𝐵 ) 𝑌 ) )
9	8	rbaib	⊢ ( 𝑋 ( 𝐵 × 𝐵 ) 𝑌 → ( 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 ↔ 𝑋 ( le ‘ 𝐾 ) 𝑌 ) )
10	7 9	syl	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 ↔ 𝑋 ( le ‘ 𝐾 ) 𝑌 ) )
11	5	ancomd	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
12		brxp	⊢ ( 𝑌 ( 𝐵 × 𝐵 ) 𝑋 ↔ ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
13	11 12	sylibr	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( 𝐵 × 𝐵 ) 𝑋 )
14		brin	⊢ ( 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 ↔ ( 𝑌 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑌 ( 𝐵 × 𝐵 ) 𝑋 ) )
15	14	rbaib	⊢ ( 𝑌 ( 𝐵 × 𝐵 ) 𝑋 → ( 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 ↔ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) )
16	13 15	syl	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 ↔ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) )
17	10 16	orbi12d	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 ∨ 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 ) ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∨ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) ) )
18	4 17	mpbird	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 ∨ 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 ) )
19	2	breqi	⊢ ( 𝑋 ≤ 𝑌 ↔ 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 )
20	2	breqi	⊢ ( 𝑌 ≤ 𝑋 ↔ 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 )
21	19 20	orbi12i	⊢ ( ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) ↔ ( 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 ∨ 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 ) )
22	18 21	sylibr	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ∨ 𝑌 ≤ 𝑋 ) )