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 ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A⋖ℋB→A⊆C∧C⊂B→C=A

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→A=C↔¬A⊆C∧C⊂B∧¬A=C
3 eqcom ⊢C=A↔A=C
4 3 imbi2i ⊢A⊆C∧C⊂B→C=A↔A⊆C∧C⊂B→A=C
5 dfpss2 ⊢A⊂C↔A⊆C∧¬A=C
6 5 anbi1i ⊢A⊂C∧C⊂B↔A⊆C∧¬A=C∧C⊂B
7 an32 ⊢A⊆C∧¬A=C∧C⊂B↔A⊆C∧C⊂B∧¬A=C
8 6 7 bitri ⊢A⊂C∧C⊂B↔A⊆C∧C⊂B∧¬A=C
9 8 notbii ⊢¬A⊂C∧C⊂B↔¬A⊆C∧C⊂B∧¬A=C
10 2 4 9 3bitr4ri ⊢¬A⊂C∧C⊂B↔A⊆C∧C⊂B→C=A
11 1 10 imbitrdi ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A⋖ℋB→A⊆C∧C⊂B→C=A