Theorem cvrnbtwn2

Description: The covers relation implies no in-betweenness. ( cvnbtwn2 analog.) (Contributed by NM, 17-Nov-2011)

	Ref	Expression
Hypotheses	cvrletr.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cvrletr.l	⊢ ≤ = ( le ‘ 𝐾 )
	cvrletr.s	⊢ < = ( lt ‘ 𝐾 )
	cvrletr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion	cvrnbtwn2	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) ↔ 𝑍 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		cvrletr.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cvrletr.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cvrletr.s	⊢ < = ( lt ‘ 𝐾 )
4		cvrletr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5	1 3 4	cvrnbtwn	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) )
6	5	3expia	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 → ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
7		iman	⊢ ( ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) → 𝑍 = 𝑌 ) ↔ ¬ ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ 𝑍 = 𝑌 ) )
8		anass	⊢ ( ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ 𝑍 = 𝑌 ) ↔ ( 𝑋 < 𝑍 ∧ ( 𝑍 ≤ 𝑌 ∧ ¬ 𝑍 = 𝑌 ) ) )
9		simpl	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝐾 ∈ Poset )
10		simpr3	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝐵 )
11		simpr2	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
12	2 3	pltval	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑍 < 𝑌 ↔ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) )
13	9 10 11 12	syl3anc	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑍 < 𝑌 ↔ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) )
14		df-ne	⊢ ( 𝑍 ≠ 𝑌 ↔ ¬ 𝑍 = 𝑌 )
15	14	anbi2i	⊢ ( ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ↔ ( 𝑍 ≤ 𝑌 ∧ ¬ 𝑍 = 𝑌 ) )
16	13 15	bitrdi	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑍 < 𝑌 ↔ ( 𝑍 ≤ 𝑌 ∧ ¬ 𝑍 = 𝑌 ) ) )
17	16	anbi2d	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ↔ ( 𝑋 < 𝑍 ∧ ( 𝑍 ≤ 𝑌 ∧ ¬ 𝑍 = 𝑌 ) ) ) )
18	8 17	bitr4id	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ 𝑍 = 𝑌 ) ↔ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
19	18	notbid	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ¬ ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ 𝑍 = 𝑌 ) ↔ ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ) )
20	7 19	syl5rbb	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ↔ ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) → 𝑍 = 𝑌 ) ) )
21	6 20	sylibd	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 → ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) → 𝑍 = 𝑌 ) ) )
22	21	3impia	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) → 𝑍 = 𝑌 ) )
23	1 3 4	cvrlt	⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )
24	23	ex	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → 𝑋 < 𝑌 ) )
25	24	3adant3r3	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 → 𝑋 < 𝑌 ) )
26	25	3impia	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )
27		breq2	⊢ ( 𝑍 = 𝑌 → ( 𝑋 < 𝑍 ↔ 𝑋 < 𝑌 ) )
28	26 27	syl5ibrcom	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑍 = 𝑌 → 𝑋 < 𝑍 ) )
29	1 2	posref	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ≤ 𝑌 )
30	29	3ad2antr2	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑌 ≤ 𝑌 )
31		breq1	⊢ ( 𝑍 = 𝑌 → ( 𝑍 ≤ 𝑌 ↔ 𝑌 ≤ 𝑌 ) )
32	30 31	syl5ibrcom	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑍 = 𝑌 → 𝑍 ≤ 𝑌 ) )
33	32	3adant3	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑍 = 𝑌 → 𝑍 ≤ 𝑌 ) )
34	28 33	jcad	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑍 = 𝑌 → ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) ) )
35	22 34	impbid	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌 ) ↔ 𝑍 = 𝑌 ) )