# Metamath Proof Explorer

## Theorem cvnbtwn

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

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 cvbr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{⋖}_{ℋ}{B}↔\left({A}\subset {B}\wedge ¬\exists {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({A}\subset {x}\wedge {x}\subset {B}\right)\right)\right)$
2 psseq2 ${⊢}{x}={C}\to \left({A}\subset {x}↔{A}\subset {C}\right)$
3 psseq1 ${⊢}{x}={C}\to \left({x}\subset {B}↔{C}\subset {B}\right)$
4 2 3 anbi12d ${⊢}{x}={C}\to \left(\left({A}\subset {x}\wedge {x}\subset {B}\right)↔\left({A}\subset {C}\wedge {C}\subset {B}\right)\right)$
5 4 rspcev ${⊢}\left({C}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\subset {C}\wedge {C}\subset {B}\right)\right)\to \exists {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({A}\subset {x}\wedge {x}\subset {B}\right)$
6 5 ex ${⊢}{C}\in {\mathbf{C}}_{ℋ}\to \left(\left({A}\subset {C}\wedge {C}\subset {B}\right)\to \exists {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({A}\subset {x}\wedge {x}\subset {B}\right)\right)$
7 6 con3rr3 ${⊢}¬\exists {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({A}\subset {x}\wedge {x}\subset {B}\right)\to \left({C}\in {\mathbf{C}}_{ℋ}\to ¬\left({A}\subset {C}\wedge {C}\subset {B}\right)\right)$
8 7 adantl ${⊢}\left({A}\subset {B}\wedge ¬\exists {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({A}\subset {x}\wedge {x}\subset {B}\right)\right)\to \left({C}\in {\mathbf{C}}_{ℋ}\to ¬\left({A}\subset {C}\wedge {C}\subset {B}\right)\right)$
9 1 8 syl6bi ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{⋖}_{ℋ}{B}\to \left({C}\in {\mathbf{C}}_{ℋ}\to ¬\left({A}\subset {C}\wedge {C}\subset {B}\right)\right)\right)$
10 9 com23 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({C}\in {\mathbf{C}}_{ℋ}\to \left({A}{⋖}_{ℋ}{B}\to ¬\left({A}\subset {C}\wedge {C}\subset {B}\right)\right)\right)$
11 10 3impia ${⊢}\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)$