# Metamath Proof Explorer

## Theorem cvnbtwn3

Description: The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvnbtwn3 ${⊢}\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}\subset {B}\right)\to {C}={A}\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}\subset {B}\right)\to {A}={C}\right)↔¬\left(\left({A}\subseteq {C}\wedge {C}\subset {B}\right)\wedge ¬{A}={C}\right)$
3 eqcom ${⊢}{C}={A}↔{A}={C}$
4 3 imbi2i ${⊢}\left(\left({A}\subseteq {C}\wedge {C}\subset {B}\right)\to {C}={A}\right)↔\left(\left({A}\subseteq {C}\wedge {C}\subset {B}\right)\to {A}={C}\right)$
5 dfpss2 ${⊢}{A}\subset {C}↔\left({A}\subseteq {C}\wedge ¬{A}={C}\right)$
6 5 anbi1i ${⊢}\left({A}\subset {C}\wedge {C}\subset {B}\right)↔\left(\left({A}\subseteq {C}\wedge ¬{A}={C}\right)\wedge {C}\subset {B}\right)$
7 an32 ${⊢}\left(\left({A}\subseteq {C}\wedge ¬{A}={C}\right)\wedge {C}\subset {B}\right)↔\left(\left({A}\subseteq {C}\wedge {C}\subset {B}\right)\wedge ¬{A}={C}\right)$
8 6 7 bitri ${⊢}\left({A}\subset {C}\wedge {C}\subset {B}\right)↔\left(\left({A}\subseteq {C}\wedge {C}\subset {B}\right)\wedge ¬{A}={C}\right)$
9 8 notbii ${⊢}¬\left({A}\subset {C}\wedge {C}\subset {B}\right)↔¬\left(\left({A}\subseteq {C}\wedge {C}\subset {B}\right)\wedge ¬{A}={C}\right)$
10 2 4 9 3bitr4ri ${⊢}¬\left({A}\subset {C}\wedge {C}\subset {B}\right)↔\left(\left({A}\subseteq {C}\wedge {C}\subset {B}\right)\to {C}={A}\right)$
11 1 10 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}\subset {B}\right)\to {C}={A}\right)\right)$