Theorem cvnbtwn4 12692

Description: The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31.

Assertion

Ref	Expression
cvnbtwn4	|- ((A e. CH /\ B e. CH /\ C e. CH) -> (A <oℋ B -> ((A C_ C /\ C C_ B) -> (C = A \/ C = B))))

Proof of Theorem cvnbtwn4

Step	Hyp	Ref	Expression
1		cvnbtwn 12689	. 2 |- ((A e. CH /\ B e. CH /\ C e. CH) -> (A <oℋ B -> -. (A C. C /\ C C. B)))
2		iman 363	. . 3 |- (((A C_ C /\ C C_ B) -> (C = A \/ C = B)) <-> -. ((A C_ C /\ C C_ B) /\ -. (C = A \/ C = B)))
3		an4 882	. . . . 5 |- (((A C_ C /\ C C_ B) /\ (-. A = C /\ -. C = B)) <-> ((A C_ C /\ -. A = C) /\ (C C_ B /\ -. C = B)))
4		ioran 424	. . . . . . 7 |- (-. (C = A \/ C = B) <-> (-. C = A /\ -. C = B))
5		eqcom 2143	. . . . . . . . 9 |- (C = A <-> A = C)
6	5	notbii 300	. . . . . . . 8 |- (-. C = A <-> -. A = C)
7	6	anbi1i 709	. . . . . . 7 |- ((-. C = A /\ -. C = B) <-> (-. A = C /\ -. C = B))
8	4, 7	bitri 279	. . . . . 6 |- (-. (C = A \/ C = B) <-> (-. A = C /\ -. C = B))
9	8	anbi2i 708	. . . . 5 |- (((A C_ C /\ C C_ B) /\ -. (C = A \/ C = B)) <-> ((A C_ C /\ C C_ B) /\ (-. A = C /\ -. C = B)))
10		dfpss2 2919	. . . . . 6 |- (A C. C <-> (A C_ C /\ -. A = C))
11		dfpss2 2919	. . . . . 6 |- (C C. B <-> (C C_ B /\ -. C = B))
12	10, 11	anbi12i 710	. . . . 5 |- ((A C. C /\ C C. B) <-> ((A C_ C /\ -. A = C) /\ (C C_ B /\ -. C = B)))
13	3, 9, 12	3bitr4i 295	. . . 4 |- (((A C_ C /\ C C_ B) /\ -. (C = A \/ C = B)) <-> (A C. C /\ C C. B))
14	13	notbii 300	. . 3 |- (-. ((A C_ C /\ C C_ B) /\ -. (C = A \/ C = B)) <-> -. (A C. C /\ C C. B))
15	2, 14	bitr2i 281	. 2 |- (-. (A C. C /\ C C. B) <-> ((A C_ C /\ C C_ B) -> (C = A \/ C = B)))
16	1, 15	syl6ib 261	1 |- ((A e. CH /\ B e. CH /\ C e. CH) -> (A <oℋ B -> ((A C_ C /\ C C_ B) -> (C = A \/ C = B))))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 336   /\ wa 337   /\ w3a 1102   = wceq 1586   e. wcel 1588   C_ wss 2827   C. wpss 2828   class class class wbr 3507  CHcch 11268   <o_ℋ ccv 11304

This theorem is referenced by:  cvmdi 12727

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-br 3508  df-opab 3566  df-cv 12682

Copyright terms: Public domain