# Metamath Proof Explorer

## Theorem cvnbtwn4

Description: The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of MaedaMaeda p. 31. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvnbtwn4 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{⋖}_{ℋ}{B}\to \left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\to \left({C}={A}\vee {C}={B}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 cvnbtwn ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{⋖}_{ℋ}{B}\to ¬\left({A}\subset {C}\wedge {C}\subset {B}\right)\right)$
2 iman ${⊢}\left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\to \left({C}={A}\vee {C}={B}\right)\right)↔¬\left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\wedge ¬\left({C}={A}\vee {C}={B}\right)\right)$
3 an4 ${⊢}\left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\wedge \left(¬{A}={C}\wedge ¬{C}={B}\right)\right)↔\left(\left({A}\subseteq {C}\wedge ¬{A}={C}\right)\wedge \left({C}\subseteq {B}\wedge ¬{C}={B}\right)\right)$
4 ioran ${⊢}¬\left({C}={A}\vee {C}={B}\right)↔\left(¬{C}={A}\wedge ¬{C}={B}\right)$
5 eqcom ${⊢}{C}={A}↔{A}={C}$
6 5 notbii ${⊢}¬{C}={A}↔¬{A}={C}$
7 6 anbi1i ${⊢}\left(¬{C}={A}\wedge ¬{C}={B}\right)↔\left(¬{A}={C}\wedge ¬{C}={B}\right)$
8 4 7 bitri ${⊢}¬\left({C}={A}\vee {C}={B}\right)↔\left(¬{A}={C}\wedge ¬{C}={B}\right)$
9 8 anbi2i ${⊢}\left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\wedge ¬\left({C}={A}\vee {C}={B}\right)\right)↔\left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\wedge \left(¬{A}={C}\wedge ¬{C}={B}\right)\right)$
10 dfpss2 ${⊢}{A}\subset {C}↔\left({A}\subseteq {C}\wedge ¬{A}={C}\right)$
11 dfpss2 ${⊢}{C}\subset {B}↔\left({C}\subseteq {B}\wedge ¬{C}={B}\right)$
12 10 11 anbi12i ${⊢}\left({A}\subset {C}\wedge {C}\subset {B}\right)↔\left(\left({A}\subseteq {C}\wedge ¬{A}={C}\right)\wedge \left({C}\subseteq {B}\wedge ¬{C}={B}\right)\right)$
13 3 9 12 3bitr4i ${⊢}\left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\wedge ¬\left({C}={A}\vee {C}={B}\right)\right)↔\left({A}\subset {C}\wedge {C}\subset {B}\right)$
14 13 notbii ${⊢}¬\left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\wedge ¬\left({C}={A}\vee {C}={B}\right)\right)↔¬\left({A}\subset {C}\wedge {C}\subset {B}\right)$
15 2 14 bitr2i ${⊢}¬\left({A}\subset {C}\wedge {C}\subset {B}\right)↔\left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\to \left({C}={A}\vee {C}={B}\right)\right)$
16 1 15 syl6ib ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{⋖}_{ℋ}{B}\to \left(\left({A}\subseteq {C}\wedge {C}\subseteq {B}\right)\to \left({C}={A}\vee {C}={B}\right)\right)\right)$