Metamath Proof Explorer

Theorem btwnconn1

Description: Connectitivy law for betweenness. Theorem 5.1 of Schwabhauser p. 39-41. (Contributed by Scott Fenton, 9-Oct-2013)

Ref Expression
Assertion btwnconn1 ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝐵 = 𝐶 → ( 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ↔ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
2 1 3anbi3d ⊢ ( 𝐵 = 𝐶 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ↔ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) )
3 orc ⊢ ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
4 3 3ad2ant3 ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
5 2 4 syl6bi ⊢ ( 𝐵 = 𝐶 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )
6 5 adantld ⊢ ( 𝐵 = 𝐶 → ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )
7 simpr1 ⊢ ( ( 𝐵 ≠ 𝐶 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐴 ≠ 𝐵 )
8 simpl ⊢ ( ( 𝐵 ≠ 𝐶 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → 𝐵 ≠ 𝐶 )
9 3simpc ⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
10 9 adantl ⊢ ( ( 𝐵 ≠ 𝐶 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) )
11 7 8 10 jca31 ⊢ ( ( 𝐵 ≠ 𝐶 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) )
12 btwnconn1lem14 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ) ∧ ( 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
13 11 12 sylan2 ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐵 ≠ 𝐶 ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
14 13 an12s ⊢ ( ( 𝐵 ≠ 𝐶 ∧ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
15 14 ex ⊢ ( 𝐵 ≠ 𝐶 → ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )
16 6 15 pm2.61ine ⊢ ( ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) )
17 16 ex ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐵 ∈ ( 𝔼 ‘ 𝑁 ) ) ∧ ( 𝐶 ∈ ( 𝔼 ‘ 𝑁 ) ∧ 𝐷 ∈ ( 𝔼 ‘ 𝑁 ) ) ) → ( ( 𝐴 ≠ 𝐵 ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐶 ⟩ ∧ 𝐵 Btwn ⟨ 𝐴 , 𝐷 ⟩ ) → ( 𝐶 Btwn ⟨ 𝐴 , 𝐷 ⟩ ∨ 𝐷 Btwn ⟨ 𝐴 , 𝐶 ⟩ ) ) )