This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌 ) ↔ 𝑋 = 𝑍 ) )