Metamath Proof Explorer

Theorem cvnbtwn2

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

Ref Expression
Assertion cvnbtwn2 ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A⋖ℋB→A⊂C∧C⊆B→C=B

Proof

Step Hyp Ref Expression
1 cvnbtwn ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A⋖ℋB→¬A⊂C∧C⊂B
2 iman ⊢A⊂C∧C⊆B→C=B↔¬A⊂C∧C⊆B∧¬C=B
3 anass ⊢A⊂C∧C⊆B∧¬C=B↔A⊂C∧C⊆B∧¬C=B
4 dfpss2 ⊢C⊂B↔C⊆B∧¬C=B
5 4 anbi2i ⊢A⊂C∧C⊂B↔A⊂C∧C⊆B∧¬C=B
6 3 5 bitr4i ⊢A⊂C∧C⊆B∧¬C=B↔A⊂C∧C⊂B
7 6 notbii ⊢¬A⊂C∧C⊆B∧¬C=B↔¬A⊂C∧C⊂B
8 2 7 bitr2i ⊢¬A⊂C∧C⊂B↔A⊂C∧C⊆B→C=B
9 1 8 imbitrdi ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A⋖ℋB→A⊂C∧C⊆B→C=B