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