Metamath Proof Explorer

Theorem tgbtwnconn3

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

Ref Expression
Hypotheses tgbtwnconn.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgbtwnconn.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgbtwnconn.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgbtwnconn.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgbtwnconn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgbtwnconn.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgbtwnconn.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgbtwnconn3.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
tgbtwnconn3.2 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
Assertion tgbtwnconn3 ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 tgbtwnconn.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgbtwnconn.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tgbtwnconn.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
4 tgbtwnconn.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
5 tgbtwnconn.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
6 tgbtwnconn.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
7 tgbtwnconn.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
8 tgbtwnconn3.1 ⊢ ( 𝜑 → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
9 tgbtwnconn3.2 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
10 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
11 3 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐺 ∈ TarskiG )
12 5 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐵 ∈ 𝑃 )
13 4 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐴 ∈ 𝑃 )
14 6 adantr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐶 ∈ 𝑃 )
15 simpr ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( ♯ ‘ 𝑃 ) = 1 )
16 1 10 2 11 12 13 14 15 tgldim0itv ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
17 16 orcd ⊢ ( ( 𝜑 ∧ ( ♯ ‘ 𝑃 ) = 1 ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
18 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐺 ∈ TarskiG )
19 simplr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝑝 ∈ 𝑃 )
20 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐴 ∈ 𝑃 )
21 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐵 ∈ 𝑃 )
22 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐶 ∈ 𝑃 )
23 simprr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐴 ≠ 𝑝 )
24 23 necomd ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝑝 ≠ 𝐴 )
25 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐷 ∈ 𝑃 )
26 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐷 ) )
27 simprl ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) )
28 1 10 2 18 25 20 19 27 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐴 ∈ ( 𝑝 𝐼 𝐷 ) )
29 1 10 2 18 21 20 19 25 26 28 tgbtwnintr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐴 ∈ ( 𝐵 𝐼 𝑝 ) )
30 1 10 2 18 21 20 19 29 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐴 ∈ ( 𝑝 𝐼 𝐵 ) )
31 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
32 1 10 2 18 20 22 25 31 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐶 ∈ ( 𝐷 𝐼 𝐴 ) )
33 1 10 2 18 25 22 20 19 32 27 tgbtwnexch3 ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐴 ∈ ( 𝐶 𝐼 𝑝 ) )
34 1 10 2 18 22 20 19 33 tgbtwncom ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → 𝐴 ∈ ( 𝑝 𝐼 𝐶 ) )
35 1 2 18 19 20 21 22 24 30 34 tgbtwnconn2 ⊢ ( ( ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
36 3 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐺 ∈ TarskiG )
37 7 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐷 ∈ 𝑃 )
38 4 adantr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 𝐴 ∈ 𝑃 )
39 simpr ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → 2 ≤ ( ♯ ‘ 𝑃 ) )
40 1 10 2 36 37 38 39 tgbtwndiff ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ∃ 𝑝 ∈ 𝑃 ( 𝐴 ∈ ( 𝐷 𝐼 𝑝 ) ∧ 𝐴 ≠ 𝑝 ) )
41 35 40 r19.29a ⊢ ( ( 𝜑 ∧ 2 ≤ ( ♯ ‘ 𝑃 ) ) → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )
42 1 4 tgldimor ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑃 ) = 1 ∨ 2 ≤ ( ♯ ‘ 𝑃 ) ) )
43 17 41 42 mpjaodan ⊢ ( 𝜑 → ( 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ∨ 𝐶 ∈ ( 𝐴 𝐼 𝐵 ) ) )