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 ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A⋖ℋB→A⊆C∧C⊆B→C=A∨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=A∨C=B↔¬A⊆C∧C⊆B∧¬C=A∨C=B
3 an4 ⊢A⊆C∧C⊆B∧¬A=C∧¬C=B↔A⊆C∧¬A=C∧C⊆B∧¬C=B
4 ioran ⊢¬C=A∨C=B↔¬C=A∧¬C=B
5 eqcom ⊢C=A↔A=C
6 5 notbii ⊢¬C=A↔¬A=C
7 6 anbi1i ⊢¬C=A∧¬C=B↔¬A=C∧¬C=B
8 4 7 bitri ⊢¬C=A∨C=B↔¬A=C∧¬C=B
9 8 anbi2i ⊢A⊆C∧C⊆B∧¬C=A∨C=B↔A⊆C∧C⊆B∧¬A=C∧¬C=B
10 dfpss2 ⊢A⊂C↔A⊆C∧¬A=C
11 dfpss2 ⊢C⊂B↔C⊆B∧¬C=B
12 10 11 anbi12i ⊢A⊂C∧C⊂B↔A⊆C∧¬A=C∧C⊆B∧¬C=B
13 3 9 12 3bitr4i ⊢A⊆C∧C⊆B∧¬C=A∨C=B↔A⊂C∧C⊂B
14 13 notbii ⊢¬A⊆C∧C⊆B∧¬C=A∨C=B↔¬A⊂C∧C⊂B
15 2 14 bitr2i ⊢¬A⊂C∧C⊂B↔A⊆C∧C⊆B→C=A∨C=B
16 1 15 imbitrdi ⊢A∈Cℋ∧B∈Cℋ∧C∈Cℋ→A⋖ℋB→A⊆C∧C⊆B→C=A∨C=B