This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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