Metamath Proof Explorer

Theorem cvrnbtwn4

Description: The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of MaedaMaeda p. 31. ( cvnbtwn4 analog.) (Contributed by NM, 18-Oct-2011)

Ref Expression
Hypotheses cvrle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrle.l ⊢ ≤ = ( le ‘ 𝐾 )
cvrle.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion cvrnbtwn4 ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ↔ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 cvrle.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrle.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvrle.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
5 1 4 3 cvrnbtwn ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ¬ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) )
6 iman ⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) → ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ↔ ¬ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) )
7 neanior ⊢ ( ( 𝑋 ≠ 𝑍 ∧ 𝑍 ≠ 𝑌 ) ↔ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) )
8 7 anbi2i ⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ( 𝑋 ≠ 𝑍 ∧ 𝑍 ≠ 𝑌 ) ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) )
9 an4 ⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ( 𝑋 ≠ 𝑍 ∧ 𝑍 ≠ 𝑌 ) ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) )
10 8 9 bitr3i ⊢ ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) )
11 2 4 pltval ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ↔ ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) )
12 11 3adant3r2 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ↔ ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ) )
13 2 4 pltval ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑍 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) )
14 13 3com23 ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑍 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) )
15 14 3adant3r1 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑍 ( lt ‘ 𝐾 ) 𝑌 ↔ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) )
16 12 15 anbi12d ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑋 ≠ 𝑍 ) ∧ ( 𝑍 ≤ 𝑌 ∧ 𝑍 ≠ 𝑌 ) ) ) )
17 10 16 bitr4id ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ) )
18 17 notbid ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ¬ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ∧ ¬ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ↔ ¬ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ) )
19 6 18 bitr2id ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ¬ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) → ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ) )
20 19 3adant3 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ¬ ( 𝑋 ( lt ‘ 𝐾 ) 𝑍 ∧ 𝑍 ( lt ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) → ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) ) )
21 5 20 mpbid ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) → ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) )
22 1 2 posref ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑍 ∈ 𝐵 ) → 𝑍 ≤ 𝑍 )
23 22 3ad2antr3 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ≤ 𝑍 )
24 23 3adant3 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑍 ≤ 𝑍 )
25 breq1 ⊢ ( 𝑋 = 𝑍 → ( 𝑋 ≤ 𝑍 ↔ 𝑍 ≤ 𝑍 ) )
26 24 25 syl5ibrcom ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 = 𝑍 → 𝑋 ≤ 𝑍 ) )
27 1 2 3 cvrle ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ≤ 𝑌 )
28 27 ex ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → 𝑋 ≤ 𝑌 ) )
29 28 3adant3r3 ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑌 → 𝑋 ≤ 𝑌 ) )
30 29 3impia ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ≤ 𝑌 )
31 breq2 ⊢ ( 𝑍 = 𝑌 → ( 𝑋 ≤ 𝑍 ↔ 𝑋 ≤ 𝑌 ) )
32 30 31 syl5ibrcom ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑍 = 𝑌 → 𝑋 ≤ 𝑍 ) )
33 26 32 jaod ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) → 𝑋 ≤ 𝑍 ) )
34 breq1 ⊢ ( 𝑋 = 𝑍 → ( 𝑋 ≤ 𝑌 ↔ 𝑍 ≤ 𝑌 ) )
35 30 34 syl5ibcom ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑋 = 𝑍 → 𝑍 ≤ 𝑌 ) )
36 breq2 ⊢ ( 𝑍 = 𝑌 → ( 𝑍 ≤ 𝑍 ↔ 𝑍 ≤ 𝑌 ) )
37 24 36 syl5ibcom ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑍 = 𝑌 → 𝑍 ≤ 𝑌 ) )
38 35 37 jaod ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) → 𝑍 ≤ 𝑌 ) )
39 33 38 jcad ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) → ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ) )
40 21 39 impbid ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌 ) ↔ ( 𝑋 = 𝑍 ∨ 𝑍 = 𝑌 ) ) )