Theorem cvrnbtwn3

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

	Ref	Expression
Hypotheses	cvrletr.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cvrletr.l	⊢ ≤ = ( le ‘ 𝐾 )
	cvrletr.s	⊢ < = ( lt ‘ 𝐾 )
	cvrletr.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion	cvrnbtwn3	⊢ ( ( 𝐾 ∈ 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	2 3	pltval	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 < 𝑍 ↔ ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) )
7	6	3adant3r2	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 < 𝑍 ↔ ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) )
8	7	3adant3	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 < 𝑍 ↔ ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) )
9	8	anbi1d	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ 𝑍 < 𝑌 ) ) )
10	9	notbid	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ↔ ¬ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ 𝑍 < 𝑌 ) ) )
11		an32	⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ 𝑍 < 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) ∧ 𝑋 ≠ 𝑍 ) )
12		df-ne	⊢ ( 𝑋 ≠ 𝑍 ↔ ¬ 𝑋 = 𝑍 )
13	12	anbi2i	⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) ∧ 𝑋 ≠ 𝑍 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) ∧ ¬ 𝑋 = 𝑍 ) )
14	11 13	bitri	⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ 𝑍 < 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) ∧ ¬ 𝑋 = 𝑍 ) )
15	14	notbii	⊢ ( ¬ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ 𝑍 < 𝑌 ) ↔ ¬ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) ∧ ¬ 𝑋 = 𝑍 ) )
16		iman	⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) → 𝑋 = 𝑍 ) ↔ ¬ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) ∧ ¬ 𝑋 = 𝑍 ) )
17	15 16	bitr4i	⊢ ( ¬ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ 𝑍 < 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) → 𝑋 = 𝑍 ) )
18	10 17	bitrdi	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ¬ ( 𝑋 < 𝑍 ∧ 𝑍 < 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) → 𝑋 = 𝑍 ) ) )
19	5 18	mpbid	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) → 𝑋 = 𝑍 ) )
20	1 2	posref	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
21		breq2	⊢ ( 𝑋 = 𝑍 → ( 𝑋 ≤ 𝑋 ↔ 𝑋 ≤ 𝑍 ) )
22	20 21	syl5ibcom	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 = 𝑍 → 𝑋 ≤ 𝑍 ) )
23	22	3ad2antr1	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 = 𝑍 → 𝑋 ≤ 𝑍 ) )
24	23	3adant3	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 = 𝑍 → 𝑋 ≤ 𝑍 ) )
25		simp1	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝐾 ∈ Poset )
26		simp21	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ∈ 𝐵 )
27		simp22	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ 𝐵 )
28		simp3	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 𝐶 𝑌 )
29	1 3 4	cvrlt	⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )
30	25 26 27 28 29	syl31anc	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )
31		breq1	⊢ ( 𝑋 = 𝑍 → ( 𝑋 < 𝑌 ↔ 𝑍 < 𝑌 ) )
32	30 31	syl5ibcom	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 = 𝑍 → 𝑍 < 𝑌 ) )
33	24 32	jcad	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 = 𝑍 → ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) ) )
34	19 33	impbid	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) ↔ 𝑋 = 𝑍 ) )