Metamath Proof Explorer

Theorem tgbtwnconn2

Description: Another connectivity law for betweenness. Theorem 5.2 of Schwabhauser p. 41. (Contributed by Thierry Arnoux, 17-May-2019)

Ref Expression
Hypotheses tgbtwnconn.p ⊢ P = Base G
tgbtwnconn.i ⊢ I = Itv ⁡ G
tgbtwnconn.g ⊢ φ → G ∈ 𝒢 Tarski
tgbtwnconn.a ⊢ φ → A ∈ P
tgbtwnconn.b ⊢ φ → B ∈ P
tgbtwnconn.c ⊢ φ → C ∈ P
tgbtwnconn.d ⊢ φ → D ∈ P
tgbtwnconn2.1 ⊢ φ → A ≠ B
tgbtwnconn2.2 ⊢ φ → B ∈ A I C
tgbtwnconn2.3 ⊢ φ → B ∈ A I D
Assertion tgbtwnconn2 ⊢ φ → C ∈ B I D ∨ D ∈ B I C

Proof

Step Hyp Ref Expression
1 tgbtwnconn.p ⊢ P = Base G
2 tgbtwnconn.i ⊢ I = Itv ⁡ G
3 tgbtwnconn.g ⊢ φ → G ∈ 𝒢 Tarski
4 tgbtwnconn.a ⊢ φ → A ∈ P
5 tgbtwnconn.b ⊢ φ → B ∈ P
6 tgbtwnconn.c ⊢ φ → C ∈ P
7 tgbtwnconn.d ⊢ φ → D ∈ P
8 tgbtwnconn2.1 ⊢ φ → A ≠ B
9 tgbtwnconn2.2 ⊢ φ → B ∈ A I C
10 tgbtwnconn2.3 ⊢ φ → B ∈ A I D
11 eqid ⊢ dist ⁡ G = dist ⁡ G
12 3 adantr ⊢ φ ∧ C ∈ A I D → G ∈ 𝒢 Tarski
13 4 adantr ⊢ φ ∧ C ∈ A I D → A ∈ P
14 5 adantr ⊢ φ ∧ C ∈ A I D → B ∈ P
15 6 adantr ⊢ φ ∧ C ∈ A I D → C ∈ P
16 7 adantr ⊢ φ ∧ C ∈ A I D → D ∈ P
17 9 adantr ⊢ φ ∧ C ∈ A I D → B ∈ A I C
18 simpr ⊢ φ ∧ C ∈ A I D → C ∈ A I D
19 1 11 2 12 13 14 15 16 17 18 tgbtwnexch3 ⊢ φ ∧ C ∈ A I D → C ∈ B I D
20 19 orcd ⊢ φ ∧ C ∈ A I D → C ∈ B I D ∨ D ∈ B I C
21 3 adantr ⊢ φ ∧ D ∈ A I C → G ∈ 𝒢 Tarski
22 4 adantr ⊢ φ ∧ D ∈ A I C → A ∈ P
23 5 adantr ⊢ φ ∧ D ∈ A I C → B ∈ P
24 7 adantr ⊢ φ ∧ D ∈ A I C → D ∈ P
25 6 adantr ⊢ φ ∧ D ∈ A I C → C ∈ P
26 10 adantr ⊢ φ ∧ D ∈ A I C → B ∈ A I D
27 simpr ⊢ φ ∧ D ∈ A I C → D ∈ A I C
28 1 11 2 21 22 23 24 25 26 27 tgbtwnexch3 ⊢ φ ∧ D ∈ A I C → D ∈ B I C
29 28 olcd ⊢ φ ∧ D ∈ A I C → C ∈ B I D ∨ D ∈ B I C
30 1 2 3 4 5 6 7 8 9 10 tgbtwnconn1 ⊢ φ → C ∈ A I D ∨ D ∈ A I C
31 20 29 30 mpjaodan ⊢ φ → C ∈ B I D ∨ D ∈ B I C